proposition: Lemma to_nat_of_nat {p}{n} (h : p < n) : to_nat (of_nat_lt h) = exist _ p h.
proof: Proof. revert p h. induction n as [|n IHn]. - intros p h. destruct (Nat.nlt_0_r p h). - intros [|p] h; cbn; [|rewrite IHn]; f_equal; apply Peano_dec.le_unique. Qed.
imports: PeanoNat