+
+lemma prelattice_of_lattice_: lattice_ → prelattice.
+intro l_; apply (mk_prelattice (excess_of_lattice_ l_)); [apply (l_meet l_);]
+unfold excess_of_lattice_; try unfold apart_of_excess; simplify;
+unfold excl; simplify;
+[intro x; intro H; elim H; clear H;
+ [apply (l_meet_refl l_ x);
+ lapply (Ap≫ ? (l_meet_comm ???) t) as H; clear t;
+ lapply (l_strong_extm l_ ??? H); apply ap_symmetric; assumption
+ | lapply (Ap≪ ? (l_meet_refl ?x) t) as H; clear t;
+ lapply (l_strong_extm l_ ??? H); apply (l_meet_refl l_ x);
+ apply ap_symmetric; assumption]
+|intros 3 (x y H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x y)) H1) as H; clear H1;
+ lapply (l_strong_extm l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (l_meet_comm ???) H1); apply (ap_coreflexive ?? Hletin);
+ |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ y x)) H2) as H; clear H2;
+ lapply (l_strong_extm l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (l_meet_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
+|intros 4 (x y z H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ x (l_meet l_ y z))) H1) as H; clear H1;
+ lapply (l_strong_extm l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (eq_sym ??? (l_meet_assoc ?x y z)) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);
+ |lapply (Ap≪ ? (l_meet_refl ? (l_meet l_ (l_meet l_ x y) z)) H2) as H; clear H2;
+ lapply (l_strong_extm l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (l_meet_assoc ?x y z) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);]
+|intros (x y z H); elim H (H1 H1); clear H;
+ lapply (Ap≪ ? (l_meet_refl ??) H1) as H; clear H1;
+ lapply (l_strong_extm l_ ??? H) as H1; clear H;
+ lapply (l_strong_extm l_ ??? H1) as H; clear H1;
+ cases (ap_cotransitive ??? (l_meet l_ y z) H);[left|right|right|left] try assumption;
+ [apply ap_symmetric;apply (Ap≪ ? (l_meet_comm ???));
+ |apply (Ap≫ ? (l_meet_comm ???));
+ |apply ap_symmetric;] assumption;
+|intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
+ lapply (Ap≪ ? (l_meet_refl ??) H) as H1; clear H;
+ lapply (l_strong_extm l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
+ assumption
+|intros 3 (x y H);
+ cut (l_meet l_ x y ≈ l_meet l_ x (l_meet l_ y y)) as H1;[2:
+ intro; lapply (l_strong_extm ???? a); apply (l_meet_refl l_ y);
+ apply ap_symmetric; assumption;]
+ lapply (Ap≪ ? (eq_sym ??? H1) H); apply (l_meet_assoc l_ x y y);
+ assumption; ]
+qed.
+
+record lattice : Type ≝ {
+ lat_carr:> prelattice;
+ join: lat_carr → lat_carr → lat_carr;
+ join_refl: ∀x.join x x ≈ x;
+ join_comm: ∀x,y:lat_carr. join x y ≈ join y x;
+ join_assoc: ∀x,y,z:lat_carr. join x (join y z) ≈ join (join x y) z;
+ absorbjm: ∀f,g:lat_carr. join f (meet ? f g) ≈ f;
+ absorbmj: ∀f,g:lat_carr. meet ? f (join f g) ≈ f;
+ strong_extj: ∀x.strong_ext ? (join x)
+}.
+
+interpretation "Lattice join" 'or a b =
+ (cic:/matita/lattice/join.con _ a b).