proposition: Lemma MZ_expo_A n : MZ_expo n B = A n.
proof: Proof. Proof using Hb_nat. induction n as [ | n IHn ]. + rewrite mscal_0. unfold B, A; simpl. rewrite alpha_fix_2, alpha_fix_1, alpha_fix_0. apply M22_equal; ring. + rewrite mscal_S, IHn. apply M22_equal; simpl plus; try ring. - rewrite alpha_fix_3 with (n := S _); ring. - alpha; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)