proposition: Lemma meet_le_compat : forall w x y z : X, w<=y -> x<=z -> meet w x <= meet y z.
proof: Proof. intros. apply le_trans with (y:=meet y x). firstorder using meet_monotone_l, monotone_def. firstorder using meet_monotone_r, monotone_def. Qed.
imports: CoRN.order.PartialOrder