proposition: Lemma nat2pos_ext n m (l1 l2 : n < m) : pos.nat2pos l1 = pos.nat2pos l2.
proof: Proof. induction m in n, l1, l2 |- *; cbn. - lia. - destruct n. + reflexivity. + f_equal. eapply IHm. Qed.
imports: Lia Nat Fin Undecidability.H10.Util.Diophantine Undecidability.FRACTRAN(FRACTRAN_computable prime_seq) Undecidability.H10(fractran_dio DPRM dio_logic) Undecidability.Shared.Libs.DLW(vec)