How to prove T Z = Z for binary representation of natural numbers in Coq I have defined an Inductive in Coq for binary representation of natural numbers as follows:

Inductive bin : Type :=
  | Z : bin
  | T : bin -&gt; bin
  | M : bin -&gt; bin.


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

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


and

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
    | Z =&gt; O
    | M b' =&gt; S (mult 2 (bin_to_nat b'))
    | T b' =&gt; 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 =&gt; M Z
    | T b' =&gt; M b'
    | M b' =&gt; T (incr b')
  end.
to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z


No, you can't prove that T Z = Z because it is false:

Lemma TZ_neq_Z : T Z &lt;&gt; Z.
Proof.
  discriminate.
Qed.


Indeed, distinct constructors of an inductive type always lead to distinct terms.

That doesn't mean you can't prove that bin_to_nat is the inverse of nat_to_bin though.