proposition: Lemma cancel_of_to (r : t) : of_nat (to_nat r) = r.
proof: Proof. destruct r as [rs]. cbn. enough (H : forall m rs, to_nat' to_nat rs <= m -> of_nat' m (to_nat' to_nat rs) = rs) by now rewrite H. intros m. clear rs. induction m as [|m IH]. { intros [|? ?]; [reflexivity|cbn; lia]. } intros [|[rs] r's]; [reflexivity|]. cbn. rewrite Cantor.cancel_of_to. intros E. assert (H' := Cantor.to_nat_non_decreasing (to_nat' to_nat rs) (to_nat' to_nat r's)). now rewrite !IH by lia. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia