proposition: Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p.
proof: Proof. induction p as [|? p]; simpl. - reflexivity. - destruct (to_nat p); simpl in *. f_equal. subst p. apply of_nat_ext. Qed.
imports: PeanoNat