proposition: Lemma join_meet_modular_r : forall x y z : X, join x (meet y (join x z)) == meet (join x y) (join x z).
proof: Proof. intros. rewrite -> join_meet_distr_r. rewrite -> (join_assoc X). rewrite -> (join_idem X). reflexivity. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice