proposition: Lemma join_meet_modular_l : forall x y z : X, join (meet (join x z) y) z == meet (join x z) (join y z).
proof: Proof. intros. rewrite -> (join_comm X (meet (join x z) y) z). rewrite -> (meet_comm X (join x z) y). rewrite -> (meet_comm X (join x z) (join y z)). rewrite -> (join_comm X x z). rewrite -> (join_comm X y z). apply join_meet_modular_r. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice