proposition: Fact MU22_Diag22 a b c d x y : (a,b,c,d) ⊠ (x,z,z,y) = (a⊗x,b⊗y,c⊗x,d⊗y).
proof: Proof. Proof using R_is_ring. apply M22_equal; ring. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)