proposition: Fact A_mult u v : A (u*v)%nat = MZ_expo u (A v).
proof: Proof. Proof using Hb_nat. rewrite <- MZ_expo_A, mscal_mult; auto. f_equal; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)