proposition: Fact M22plus_zero : forall m, ZE_22 ⊞ m = m.
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)