proposition: Lemma to_nat_inj {n} (p q : t n) : proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q.
proof: Proof. intro H. rewrite <- (of_nat_to_nat_inv p), <- (of_nat_to_nat_inv q). destruct (to_nat p) as (np,hp), (to_nat q) as (nq,hq); simpl in *. revert hp hq. rewrite H. apply of_nat_ext. Qed.
imports: PeanoNat