proposition: Lemma le_meet_l : forall x y : X, x <= y <-> meet x y == x.
proof: Proof. intros. split; intros. apply le_antisym. apply meet_lb_l. apply meet_glb. apply le_refl. assumption. rewrite <- H. apply meet_lb_r. Qed.
imports: CoRN.order.PartialOrder