x y z : (x ⊓ y) ⊔ (x ⊓ z) ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) ⊓ (y ⊔ z). Proof. rewrite (distribute_r x y (x ⊓ z)), join_meet_absorption. rewrite (distribute_r _ _ (y ⊓ z)). rewrite (distribute_l x y z). rewrite (commutativity y (x ⊓ z)), <-(simple_associativity _ y). rewrite join_meet_absorption. rewrite (distribute_r x z y). rewrite (commutativity (f:=join) z y). rewrite (commutativity (x ⊔ y) (x ⊔ z)). rewrite simple_associativity, <-(simple_associativity (x ⊔ z)). rewrite (idempotency _ _). rewrite (commutativity (x ⊔ z) (x ⊔ y)). reflexivity. Qed.
Require Import