proposition: Lemma cut_minus_min3 x y z : (x + (y ⊓ z)) ∸ ((x + y) ⊓ (x + z)) = ((x + y) ⊓ (x + z)) ∸ (x + (y ⊓ z)).
proof: Proof. Proof with auto; try reflexivity. destruct (total (≤) y z) as [G1|G1]. rewrite (lattices.meet_l y z), (lattices.meet_l (x + y) (x + z))... rewrite (lattices.meet_r y z), (lattices.meet_r (x + y) (x + z))... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax