+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.
+