proposition: Lemma distribute_alt x y z : (x ⊓ y) ⊔ (x ⊓ z) ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) ⊓ (y ⊔ z).
proof: 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)), <-(associativity _ y). rewrite join_meet_absorption. rewrite (distribute_r x z y). rewrite (commutativity z y). rewrite (commutativity (x ⊔ y) (x ⊔ z)). rewrite associativity, <-(associativity (x ⊔ z)). rewrite (idempotency _ _). now rewrite (commutativity (x ⊔ z) (x ⊔ y)). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.groups