+interpretation "Metric lattice leq" 'leq a b =
+ (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b).
+interpretation "Metric lattice geq" 'geq a b =
+ (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b).
+