}.
interpretation "Metric lattice leq" 'leq a b =
- (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b).
+ (le (excess_OF_mlattice1 _ _) a b).
interpretation "Metric lattice geq" 'geq a b =
- (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b).
+ (le (excess_OF_mlattice _ _) a b).
lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
intros (R ml a b E); intro H; apply E; apply ml_prop1;