proposition: Lemma meet_lb_l : forall x y : X, meet x y <= x.
proof: Proof. Proof (sl_meet_lb_l _ _ (sl_proof X)). Lemma meet_lb_r : forall x y : X, meet x y <= y. Proof (sl_meet_lb_r _ _ (sl_proof X)). Lemma meet_glb : forall x y z : X, z <= x -> z <= y -> z <= meet x y. Proof (sl_meet_glb _ _ (sl_proof X)). Lemma meet_comm : forall x y:X, meet x y == meet y x. Proof. assert (forall x y : X, meet x y <= meet y x). intros. destruct X. simpl in *. firstorder. intros; apply le_antisym; firstorder. Qed.
imports: CoRN.order.PartialOrder