proposition: Fact M22scal_PL22 k : forall x y, M22scal k (x ⊞ y) = M22scal k x ⊞ M22scal k y.
proof: Proof. Proof using R_is_ring. myauto 2. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)