proposition: Lemma cancel_to_of n : to_nat (of_nat n) = n.
proof: Proof. induction n as [|n IHn]; [reflexivity|]. cbn. fold (of_nat n). destruct (of_nat n) as [[|x] y]. - rewrite <- IHn. cbn. now rewrite PeanoNat.Nat.add_0_r. - rewrite <- IHn. cbn. now rewrite (Nat.add_succ_r y x). Qed.
imports: PeanoNat Lia