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