proposition: Lemma cancel_to_of (n : nat) : to_nat (of_nat n) = n.
proof: Proof. enough (H : forall m n, n <= m -> to_nat' to_nat (of_nat' m n) = n) by now apply H. intros m. clear n. induction m as [|m IH]. { now intros [|?] ?; [|lia]. } intros [|n] ?; [reflexivity|]. cbn. destruct (Cantor.of_nat n) as [n1 n2] eqn:E. apply (f_equal Cantor.to_nat) in E. rewrite Cantor.cancel_to_of in E. assert (Hn := Cantor.to_nat_non_decreasing n1 n2). cbn. rewrite !IH, <- E; lia. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia