proposition: Lemma cut_minus_min1 x y z : x ∸ (y ⊓ z) = x ∸ y + ((x ⊓ y) ∸ z).
proof: Proof. Proof with eauto; try ring. unfold meet, min, sort. case (decide_rel (≤) x y); case (decide_rel (≤) y z); intros F G; simpl. rewrite (cut_minus_0 x z)... rewrite (cut_minus_0 x y)... rewrite (cut_minus_0 y z)... symmetry... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax