proposition: Fact mscal_Zplus n : mscal Zplus 0 n 1 = Z.of_nat n.
proof: Proof. induction n as [ | n IHn ]. + rewrite mscal_0; auto. + rewrite mscal_S, IHn. rewrite Nat2Z.inj_succ; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)