proposition: Fact A_plus u v : A (u+v)%nat = A u ⊠ A v.
proof: Proof. Proof using Hb_nat. rewrite <- MZ_expo_A, mscal_plus; 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)