How to prove T Z = Z for binary representation of natural numbers in Coq

Question

I have defined an Inductive in Coq for binary representation of natural numbers as follows:

Inductive bin : Type :=
  | Z : bin
  | T : bin -> bin
  | M : bin -> bin.

and two recursive functions to convert between nat and bin types as:

Fixpoint nat_to_bin (n : nat) : bin :=
  match n with
    | O => Z
    | S n' => incr (nat_to_bin n')
  end.

and

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
    | Z => O
    | M b' => S (mult 2 (bin_to_nat b'))
    | T b' => mult 2 (bin_to_nat b')
  end.

to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z by using these tactics that I know: simpl reflexivity destruct rewrite replace induction please recommend some clues showing how to do this. Thank you!

Edit

The incr implementation is

Fixpoint incr (b : bin) : bin :=
  match b with
    | Z => M Z
    | T b' => M b'
    | M b' => T (incr b')
  end.