refactoring of some lemmas, shorter proofs

[helm.git] / helm / software / matita / dama / metric_lattice.ma

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index cca6430983486656f7863db6224c02d4c7d22ed3..b5261b9dc44698b021b875f288180b741c614fb4 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -92,7 +92,8 @@ lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy
 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) + δ(x∨y) z) (meq_l ????? Dxj));
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z)) (meq_r ????? Dyj));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [
+  apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (x∨y) ? Dyj));]
 apply (Eq≈ ? (plus_comm ???));
 apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y)));
 apply feq_plusl;