proposition: Lemma fun2vec_plus {n} m {X} (f : nat -> X) : fun2vec n m f = fun2vec 0 m (fun i => f ( n + i)).
proof: Proof. induction m in n, f |- *; cbn. - reflexivity. - f_equal. + f_equal. lia. + rewrite IHm at 1. symmetry. rewrite IHm at 1. eapply fun2vec_ext. intros. f_equal. lia. 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)