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