set "baseuri" "cic:/matita/lattice/".
-include "excedence.ma".
+include "excess.ma".
record lattice : Type ≝ {
l_carr:> apartness;
definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
-lemma excedence_of_lattice: lattice → excedence.
-intro l; apply (mk_excedence l (excl l));
+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;
assumption]
qed.
-coercion cic:/matita/lattice/excedence_of_lattice.con.
+coercion cic:/matita/lattice/excess_of_lattice.con.
lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
intros (l a b H);
- unfold le in H; unfold excedence_of_lattice in H;
+ unfold le in H; unfold excess_of_lattice in H;
unfold excl in H; simplify in H;
unfold eq; assumption;
qed.