-interpretation "Lattive meet le" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b).
-
-interpretation "Lattive join le (aka ge)" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b).
-
-lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a.
-intros(l a b H); apply H;
-qed.
-
-lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b.
-intros(l a b H); apply H;
-qed.
-
-lemma eq_to_eq:∀l:lattice.∀a,b:l.
- (eq (apart_of_excess (pl_carr (latt_jcarr l))) a b) →
- (eq (apart_of_excess (pl_carr (latt_mcarr l))) a b).
-intros 3; unfold eq; unfold apartness_OF_lattice;
-unfold apartness_OF_lattice_1; unfold latt_jcarr; simplify;
-unfold dual_exc; simplify; intros 2 (H H1); apply H;
-cases H1;[right|left]assumption;
-qed.
-
-coercion cic:/matita/metric_lattice/eq_to_eq.con nocomposites.
-