proposition: Lemma join_meet_distr_r : forall x y z:X, (join x (meet y z))==(meet (join x y) (join x z)).
proof: Proof. Proof (fun a => monotone_meet_distr _ (join_monotone_r X a)). Lemma join_meet_distr_l : forall x y z:X, (join (meet y z) x)==(meet (join y x) (join z x)). Proof (fun a => monotone_meet_distr _ (join_monotone_l X a)). Section Antitone. Variable f : X -> X. Hypothesis Hf : antitone X f. Add Parametric Morphism: f with signature (@st_eq X) ==> (@st_eq X) as antitone_compat. Proof. revert Hf; rewrite -> antitone_def; intros. rewrite -> equiv_le_def in *. firstorder. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice