proposition: Theorem M22plus_monoid : monoid_theory PL22 ZE_22.
proof: Proof. Proof using R_is_ring. exists. + apply M22plus_zero. + intro; rewrite M22add_comm; apply M22plus_zero. + intros; apply M22add_assoc. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)