proposition: Fact M22plus_cancel : forall x a b, x ⊞ a = x ⊞ b -> a = b.
proof: Proof. Proof using R_is_ring. intros x a b H. rewrite <- (M22plus_zero a), <- (M22minus x), (M22add_comm x), <- M22add_assoc, H, M22add_assoc, (M22add_comm _ x), M22minus, M22plus_zero. trivial. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)