proposition: Lemma meet_assoc : forall x y z:X, meet x (meet y z) == meet (meet x y) z.
proof: Proof. assert (forall x y z : X, meet x (meet y z) <= meet (meet x y) z). intros. apply meet_glb; [apply meet_glb|]; firstorder using meet_lb_l, meet_lb_r, le_trans. intros. apply le_antisym. apply H. rewrite -> meet_comm. rewrite -> (meet_comm x (meet y z)). rewrite -> (meet_comm x y). rewrite -> (meet_comm y z). apply H. Qed.
imports: CoRN.order.PartialOrder