proposition: Lemma meet_monotone_l : forall a : X, monotone X (fun x => meet x a).
proof: Proof. intros. assert (A:=meet_monotone_r a). revert A; do 2 rewrite -> monotone_def;intros. rewrite -> (meet_comm x), (meet_comm y);auto. Qed.
imports: CoRN.order.PartialOrder