proposition: Fact alpha_nat_gt_0 : forall n, n <> 0 -> alpha_nat n <> 0.
proof: Proof. Proof using Hb_nat. intros [ | n ] H; try lia. generalize (alpha_nat_ge_n (S n)); lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)