coercion cic:/matita/metric_lattice/ml_mspace.con.
alias symbol "plus" = "Abelian group plus".
-alias symbol "leq" = "ordered sets less or equal than".
+alias symbol "leq" = "Excess less or equal than".
record mlattice (R : todgroup) : Type ≝ {
ml_carr :> mlattice_ R;
ml_prop1: ∀a,b:ml_carr. 0 < δ a b → a # b;
apply (le_transitive ????? (ml_prop2 ?? (y) ??));
cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
-lapply (le_to_eqm ?? Lxy) as Dxm; lapply (le_to_eqm ?? Lyz) as Dym;
-lapply (le_to_eqj ?? Lxy) as Dxj; lapply (le_to_eqj ?? Lyz) as Dyj; clear Lxy Lyz;
+lapply (le_to_eqm y x Lxy) as Dxm; lapply (le_to_eqm z y Lyz) as Dym;
+lapply (le_to_eqj x y Lxy) as Dxj; lapply (le_to_eqj y z Lyz) as Dyj; clear Lxy Lyz;
+STOP
apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[