proposition: Lemma meet_monotone_r : forall a : X, monotone X (meet a).
proof: Proof. intros. rewrite -> monotone_def. intros. revert H;rewrite -> le_meet_l, meet_comm; intro. rewrite <- H. rewrite -> meet_assoc. apply meet_lb_l. Qed.
imports: CoRN.order.PartialOrder