proposition: Lemma monotone_join_distr : forall f, monotone X f -> forall x y : X, f (join x y) == join (f x) (f y).
proof: Proof. Proof monotone_meet_distr Dual. Lemma meet_join_distr_r : forall x y z:X, (meet x (join y z))==(join (meet x y) (meet x z)). Proof join_meet_distr_r Dual. Lemma meet_join_distr_l : forall x y z:X, (meet (join y z) x)==(join (meet y x) (meet z x)). Proof join_meet_distr_l Dual. Lemma antitone_join_meet_distr : forall f, antitone X f -> forall x y : X, f (join x y) == meet (f x) (f y). Proof antitone_meet_join_distr Dual. Lemma meet_join_modular_r : forall x y z : X, meet x (join y (meet x z)) == join (meet x y) (meet x z). Proof join_meet_modular_r Dual. Lemma meet_join_modular_l : forall x y z : X, meet (join (meet x z) y) z == join (meet x z) (meet y z). Proof join_meet_modular_l Dual. End MaxMin. Section TotalOrderMinDef. Variable X : PartialOrder. Variable min : X -> X -> X. Hypothesis le_total : forall x y:X, {x <= y}+{y <= x}. Hypothesis min_def1 : forall x y:X, x <= y -> min x y == x. Hypothesis min_def2 : forall x y:X, y <= x -> min x y == y. Lemma min_lb_l : forall x y:X, min x y <= x. Proof. intros. destruct (le_total x y). rewrite -> min_def1; auto. apply le_refl. rewrite -> min_def2; auto. Qed.
imports: Coq.Setoids.Setoid CoRN.order.Lattice