proposition: Theorem seq_of_coprimes n i j : i <= n -> j <= n -> i <> j -> is_gcd (1+i*fact n) (1+j*fact n) 1.
proof: Proof. intros H1 H2 H3. destruct (lt_eq_lt_dec i j) as [ [] | ]; try tauto; [ | apply is_gcd_sym ]; apply seq_of_coprimes_lt; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd prime binomial) Undecidability.Shared.Libs.DLW.Vec(pos vec)