-record lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? join;
- l_associative_j: associative ? join;
- l_comm_m: symmetric ? meet;
- l_associative_m: associative ? meet;
- (* other properties *)
- l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
- l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
- }.
+lemma excess_of_lattice: lattice → excess.
+intro l; apply (mk_excess l (excl l));
+[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
+ apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
+| intros 3 (x y z); unfold excl; intro H;
+ cases (ap_cotransitive ??? (x∧z∧y) H) (H1 H2); [2:
+ left; apply ap_symmetric; apply (strong_extm ? y);
+ apply (ap_rewl ???? (meet_comm ???));
+ apply (ap_rewr ???? (meet_comm ???));
+ assumption]
+ cases (ap_cotransitive ??? (x∧z) H1) (H2 H3); [left; assumption]
+ right; apply (strong_extm ? x); apply (ap_rewr ???? (meet_assoc ????));
+ assumption]
+qed.