proposition: Lemma monotone_meet_distr : forall x y : X, f (meet x y) == meet (f x) (f y).
proof: Proof. set (Hf':=Hf). rewrite -> monotone_def in Hf'. assert (forall x y : X, x <= y -> f (meet x y) == meet (f x) (f y)). intros x y Hxy. assert (Hfxfy:=Hf' _ _ Hxy). rewrite -> le_meet_l in Hxy. rewrite -> le_meet_l in Hfxfy. rewrite -> Hfxfy. rewrite -> Hxy. reflexivity. intros. destruct (le_total _ x y). auto. rewrite -> (meet_comm X). rewrite -> (meet_comm _ (f x)). auto. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice