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