proposition: Fact mscal_M22scal n x : mscal PL22 ZE_22 n x = M22scal (mscal Rplus Rzero n Rone) x.
proof: Proof. Proof using R_is_ring. induction n as [ | n IHn ]. + do 2 rewrite mscal_0; revert x; myauto 1. + do 2 rewrite mscal_S. rewrite IHn; clear IHn. revert x; myauto 1. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)