proposition: Fact alpha_nat_2 n : b_nat = 2 -> alpha_nat n = n.
proof: Proof. Proof using Hb_nat. intros Hb. induction on n as IHn with measure n. destruct n as [ | [ | n ] ]; auto. rewrite alpha_nat_fix_2, Hb, IHn, IHn; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)