proposition: Fact A_plus_mult m n k l : (m = n + l * k)%nat -> A m = A n ⊠ MZ_expo l (A k).
proof: Proof. Proof using Hb_nat. intro; subst; rewrite A_plus, A_mult; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)