proposition: Fact alpha_SSm_m_neq_0 : v <> 0%nat.
proof: Proof. Proof using Hb_nat Hv. intros H; subst; simpl in Hv. generalize (alpha_inc m) (alpha_inc (S m)); lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)