How to prove T Z = Z for binary representation of natural numbers in Coq
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.