proposition: Lemma meet_join_disassoc : forall x y z : X, meet (join x y) z <= join x (meet y z).
proof: Proof. intros. rewrite -> join_meet_distr_r. apply meet_le_compat. apply le_refl. apply join_ub_r. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice