-record lattice : Type \def
- { l_carrier:> Type;
- l_join: l_carrier→l_carrier→l_carrier;
- l_meet: l_carrier→l_carrier→l_carrier;
- l_lattice_properties:> is_lattice ? l_join l_meet
- }.
+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.