proposition: Lemma alpha_nat_coprime n : is_gcd (alpha_nat (S n)) (alpha_nat n) 1.
proof: Proof. Proof using Hb_nat. apply Z_coprime, (A_eq_3_12 (S n)). Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)