proposition: Lemma cancel_of_to p : of_nat (to_nat p) = p.
proof: Proof. enough (H : forall n p, to_nat p = n -> of_nat n = p) by now apply H. intro n. induction n as [|n IHn]. - now intros [[|?] [|?]]. - intros [x [|y]]. + destruct x as [|x]; [discriminate|]. intros [=H]. cbn. fold (of_nat n). rewrite (IHn (0, x)); [reflexivity|]. rewrite <- H. cbn. now rewrite PeanoNat.Nat.add_0_r. + intros [=H]. cbn. fold (of_nat n). rewrite (IHn (S x, y)); [reflexivity|]. rewrite <- H. cbn. now rewrite Nat.add_succ_r. Qed.
imports: PeanoNat Lia