proposition: Lemma meet_join_absorb_l_l : forall x y:X, meet x (join x y) == x.
proof: Proof. intros. apply le_antisym. apply meet_lb_l. apply meet_glb. apply le_refl. apply join_ub_l. Qed.
imports: Coq.Setoids.Setoid CoRN.order.SemiLattice