From 39c55604f8114e2e8f9f9769acd328de8f19c7e4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 Nov 2007 14:35:21 +0000
Subject: [PATCH] cleanup of the eq_trans burdain

---
 .../matita/dama/attic/ordered_fields_ch0.ma   |   2 +-
 .../dama/classical_pointfree/ordered_sets.ma  |   4 +-
 .../dama/classical_pointfree/ordered_sets2.ma |   2 +-
 helm/software/matita/dama/excedence.ma        |  25 ++++-
 helm/software/matita/dama/group.ma            |  29 ++---
 helm/software/matita/dama/lattice.ma          |   6 +-
 helm/software/matita/dama/metric_lattice.ma   |  52 +++++----
 helm/software/matita/dama/ordered_group.ma    |  13 ---
 .../matita/dama/preweighted_lattice.ma        | 100 +++++++++---------
 9 files changed, 120 insertions(+), 113 deletions(-)

diff --git a/helm/software/matita/dama/attic/ordered_fields_ch0.ma b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
index b312c31ab..5be3c9da4 100644
--- a/helm/software/matita/dama/attic/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
@@ -18,7 +18,7 @@ include "attic/fields.ma".
 include "ordered_group.ma".
 
 (*CSC: non capisco questi alias! Una volta non servivano*)
-alias id "plus" = "cic:/matita/groups/plus.con".
+alias id "plus" = "cic:/matita/group/plus.con".
 alias symbol "plus" = "Abelian group plus".
 
 record pre_ordered_field_ch0: Type ≝
diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
index 604da01d6..127bbf696 100644
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 for @{ 'hide_everything_but $a }.
 
 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.
diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
index dafa0df4f..d85a02cf4 100644
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
@@ -61,7 +61,7 @@ theorem le_to_le_sup_sup:
 qed. 
 
 interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (cic:/matita/ordered_set/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
 
 lemma reduce_bas_seq:
  ∀O:ordered_set.∀a:nat→O.∀p.∀i.
diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 22612e2c1..42d53a5dc 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -96,7 +96,14 @@ intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy);
 [apply Exy|apply Eyz] assumption.
 qed.
 
-lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_.
+lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ 
+  λE,x,y,z.eq_trans_ E x z y.
+
+notation > "'Eq'≈" non associative with precedence 50 for
+ @{'eqrewrite}.
+ 
+interpretation "eq_rew" 'eqrewrite = 
+ (cic:/matita/excedence/eq_trans.con _ _ _).
 
 (* BUG: vedere se ricapita *)
 alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
@@ -139,11 +146,23 @@ intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
 intro Xyz; apply Exy; apply unfold_apart; right; assumption;
 qed.
 
+notation > "'Ex'≪" non associative with precedence 50 for
+ @{'excedencerewritel}.
+ 
+interpretation "exc_rewl" 'excedencerewritel = 
+ (cic:/matita/excedence/exc_rewl.con _ _ _).
+
 lemma le_rewr: ∀E:excedence.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
 intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
 intro Xyz; apply Exy; apply unfold_apart; left; assumption;
 qed.
+
+notation > "'Ex'≫" non associative with precedence 50 for
+ @{'excedencerewriter}.
  
+interpretation "exc_rewr" 'excedencerewriter = 
+ (cic:/matita/excedence/exc_rewr.con _ _ _).
+
 lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
 intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
 cases (Exy (ap_symmetric ??? a));
@@ -183,4 +202,8 @@ qed.
     
 lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
+qed.
+
+lemma ap_le_to_lt: ∀E:excedence.∀a,c:E.c # a → c ≤ a → c < a.
+intros; split; assumption;
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma
index b0c7c2e9b..87cc25855 100644
--- a/helm/software/matita/dama/group.ma
+++ b/helm/software/matita/dama/group.ma
@@ -142,37 +142,38 @@ qed.
 theorem eq_opp_plus_plus_opp_opp: 
   ∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y.
 intros (G x y); apply (plus_cancr ??? (x+y));
-apply (eq_trans ?? 0 ? (opp_inverse ??));
-apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
-apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
-apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
-apply (eq_trans ?? (-y + 0 + y)); 
+apply (Eq≈ 0 (opp_inverse ??));
+apply (Eq≈ (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
+apply (Eq≈ (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
+apply (Eq≈ (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
+apply (Eq≈ (-y + 0 + y)); 
   [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse]
-apply (eq_trans ?? (-y + y)); 
+apply (Eq≈ (-y + y)); 
   [2: apply feq_plusr; apply eq_sym; 
-      apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
+      apply (Eq≈ (0+-y)); [apply plus_comm|apply zero_neutral]]
 apply eq_sym; apply opp_inverse.
 qed.
 
 theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x.
 intros (G x); apply (plus_cancl ??? (-x));
-apply (eq_trans ?? (--x + -x)); [apply plus_comm]
-apply (eq_trans ?? 0); [apply opp_inverse]
+apply (Eq≈ (--x + -x) (plus_comm ???));
+apply (Eq≈ 0 (opp_inverse ??));
 apply eq_sym; apply opp_inverse;
 qed.
 
 theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
 intro G; apply (plus_cancr ??? 0);
-apply (eq_trans ?? 0); [apply zero_neutral;]
+apply (Eq≈ 0); [apply zero_neutral;]
 apply eq_sym; apply opp_inverse;
 qed.
 
 lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z.
 intros (G x y z H1 H2); apply (plus_cancr ??? z);
-apply (eq_trans ?? 0 ?? (opp_inverse ?z));
-apply (eq_trans ?? (-y + z) ? H2);
-apply (eq_trans ?? (-y + y) ? H1);
-apply (eq_trans ?? 0 ? (opp_inverse ??));
+(* apply (eq_trans ??? 0 ? (opp_inverse ??)); *)
+apply (Eq≈ 0 ? (opp_inverse ??));
+apply (Eq≈ (-y + z) H2);
+apply (Eq≈ (-y + y) H1);
+apply (Eq≈ 0 (opp_inverse ??));
 apply eq_reflexive;
 qed.
 
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 9e91376d1..d6b637a0d 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -77,9 +77,9 @@ qed.
 lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
 intros (l a b H); lapply (le_to_eqm ??? H) as H1;
 lapply (feq_jl ??? b H1) as H2;
-apply (eq_trans ????? (join_comm ???));
-apply (eq_trans ?? (b∨a∧b) ?? H2); clear H1 H2 H;
-apply (eq_trans ?? (b∨(b∧a)) ?? (feq_jl ???? (meet_comm ???)));
+apply (Eq≈ ?? (join_comm ???));
+apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
+apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
 apply eq_sym; apply absorbjm;
 qed.
 
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 917e2a199..a4ca3b4f4 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -54,13 +54,6 @@ apply (ml_prop1 ?? ml); split [apply mpositive] apply ap_symmetric;
 assumption;
 qed.
 
-(*
-lemma lt_to_dpos: ∀R.∀ml:mlattice R.∀x,y:ml.x < y → 0 < δ x y.
-intros 4; repeat (unfold in ⊢ (? % ? ?→?)); simplify; unfold excl;
-intro H; elim H (H1 H2); elim H2 (H3 H3); [cases (H1 H3)]
-split; [apply mpositive]
-*)
-
 lemma meq_l: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δx y ≈ δz y.
 intros (R ml x y z); apply le_le_eq;
 [ apply (le_transitive ???? (mtineq ???y z)); 
@@ -76,10 +69,7 @@ lemma meq_r: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δy x ≈ δy z.
 intros; apply (eq_trans ???? (msymmetric ??y x));
 apply (eq_trans ????? (msymmetric ??z y)); apply meq_l; assumption;
 qed.
-
-lemma ap_le_to_lt: ∀O:ogroup.∀a,c:O.c # a → c ≤ a → c < a.
-intros (R a c A L); split; assumption;
-qed. 
+ 
 
 lemma dap_to_lt: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → 0 < δ x y.
 intros; split [apply mpositive] apply ap_symmetric; assumption;
@@ -95,22 +85,28 @@ lemma le_mtri:
   ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
 intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq]
 apply (le_transitive ????? (ml_prop2 ?? ml (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;
-  apply (eq_trans ?? (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
-  apply (eq_trans ?? (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
-  apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
-  apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
-  apply (eq_trans ?? ? ? (plus_comm ???));
-  apply (eq_trans ?? (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
-  apply feq_plusl;
-  apply (eq_trans ?? (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
-  apply eq_reflexive;   
+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;
+apply (Eq≈ (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
+apply (Eq≈ ? (plus_comm ???));
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
+apply feq_plusl;
+apply (Eq≈ (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
+apply eq_reflexive;   
 qed.  
 
-
-
+(* 3.17 conclusione: δ x y ≈ 0 *)
+(* 3.20 conclusione: δ x y ≈ 0 *)
+(* 3.21 sup forte
+   strong_sup x ≝ ∀n. s n ≤ x ∧ ∀y x ≰ y → ∃n. s n ≰ y
+   strong_sup_zoli x ≝  ∀n. s n ≤ x ∧ ∄y. y#x ∧ y ≤ x
+*)
+(* 3.22 sup debole (più piccolo dei maggioranti) *)
+(* 3.23 conclusion: δ x sup(...) ≈ 0 *)
+(* 3.25 vero nel reticolo e basta (niente δ) *)
+(* 3.36 conclusion: δ x y ≈ 0 *)
\ No newline at end of file
diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 5b0f0aa9b..d2f96fb5c 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -37,18 +37,6 @@ record ogroup : Type ≝ {
   exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g
 }.
 
-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excedencerewritel}.
- 
-interpretation "exc_rewl" 'excedencerewritel = 
- (cic:/matita/excedence/exc_rewl.con _ _ _).
-
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excedencerewriter}.
- 
-interpretation "exc_rewr" 'excedencerewriter = 
- (cic:/matita/excedence/exc_rewr.con _ _ _).
-
 lemma fexc_plusr: 
   ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z.
 intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z));
@@ -196,6 +184,5 @@ apply (le_rewr ??? b (zero_neutral ??));
 assumption;
 qed.
 
-
   
   
\ No newline at end of file
diff --git a/helm/software/matita/dama/preweighted_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma
index 39105c0fd..5dbaf51ec 100644
--- a/helm/software/matita/dama/preweighted_lattice.ma
+++ b/helm/software/matita/dama/preweighted_lattice.ma
@@ -50,27 +50,27 @@ lemma feq_joinr: ∀R.∀L:wlattice R.∀x,y,z:L.
   μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
 intros (R L x y z H H1);
 apply (plus_cancr ??? (μ(z∧x)));
-apply (eq_trans ?? (μz + μx) ? (modular_mjp ????));
-apply (eq_trans ?? (μz + μy) ? H); clear H;
-apply (eq_trans ?? (μ(z∨y) + μ(z∧y)) ? (modular_mjp ??z y));
+apply (Eq≈ (μz + μx) (modular_mjp ????));
+apply (Eq≈ (μz + μy) H); clear H;
+apply (Eq≈ (μ(z∨y) + μ(z∧y)) (modular_mjp ??z y));
 apply (plus_cancl ??? (- μ (z ∨ y)));
-apply (eq_trans ?? ? ? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
-apply (eq_trans ?? ? ? (zero_neutral ??));
-apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??)); 
-apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??));
+apply (Eq≈ ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(z∧y)) (opp_inverse ??));
+apply (Eq≈ ? (zero_neutral ??));
+apply (Eq≈ (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(z∧x)) ? (opp_inverse ??)); 
+apply (Eq≈ (μ (z ∧ x)) H1 (zero_neutral ??));
 qed.
 
 lemma modularj: ∀R.∀L:wlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
 intros (R L y z);
 lapply (modular_mjp ?? y z) as H1;
 apply (plus_cancr ??? (μ(y ∧ z)));
-apply (eq_trans ?? ? ? H1); clear H1;
-apply (eq_trans ?? ? ?? (plus_assoc ????));   
-apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));   
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply (Eq≈ ? H1); clear H1;
+apply (Eq≈ ?? (plus_assoc ????));   
+apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));   
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
 qed.
 
@@ -80,63 +80,63 @@ lemma modularm: ∀R.∀L:wlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y
 intros (R L y z);
 lapply (modular_mjp ?? y z) as H1;
 apply (plus_cancl ??? (μ(y ∨ z)));
-apply (eq_trans ?? ? ? H1); clear H1;
-apply (eq_trans ????? (plus_comm ???));
-apply (eq_trans ?? ? ?? (plus_assoc ????));    
-apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));   
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply (Eq≈ ? H1); clear H1;
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ ?? (plus_assoc ????));    
+apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));   
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
 qed.
 
 lemma modularmj: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∨ z)) as H1;
-apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? (feq_plusr ???? H1)); clear H1;
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
-apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??));
+apply (Eq≈ (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ? (feq_plusr ???? H1)); clear H1;
+apply (Eq≈ ? ? (plus_comm ???));
+apply (Eq≈ (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ? (plus_assoc ????));
+apply (Eq≈ (0+μ(x∧(y∨z))) ? (opp_inverse ??));
+apply (Eq≈ (μ(x∧(y∨z))) ? (zero_neutral ??));
 apply eq_reflexive.
 qed.
 
 lemma modularjm: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∧ z)) as H1;
-apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
+apply (Eq≈ (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
+apply (Eq≈ ? ? (plus_comm ???));
+apply (Eq≈ (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(x∨y∧z)) ? (opp_inverse ??));
 apply eq_sym; apply zero_neutral;
 qed.
 
 lemma step1_3_57': ∀R.∀L:wlattice R.∀x,y,z:L.
   μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
 intros (R L x y z);
-apply (eq_trans ?? ? ? (modularjm ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
+apply (Eq≈ ? (modularjm ?? x y z));
+apply (Eq≈ ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z)))); [
   apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
+apply (Eq≈ (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
   apply feq_plusl; apply feq_opp;
-  apply (eq_trans ?? ? ? (meet_assoc ?????));
-  apply (eq_trans ?? ? ? (meet_comm ????));
+  apply (Eq≈ ? (meet_assoc ?????));
+  apply (Eq≈ ? (meet_comm ????));
   apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
 apply feq_plusr; apply plus_assoc;
 qed.
 
 lemma step1_3_57: ∀R.∀L:wlattice R.∀x,y,z:L.
   μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
 intros (R L x y z);
-apply (eq_trans ?? ? ? (modularmj ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
+apply (Eq≈ ? (modularmj ?? x y z));
+apply (Eq≈ ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z)))); [
   apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
+apply (Eq≈ (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
   apply feq_plusl; apply feq_opp;
-  apply (eq_trans ?? ? ? (join_assoc ?????));
-  apply (eq_trans ?? ? ? (join_comm ????));
+  apply (Eq≈ ? (join_assoc ?????));
+  apply (Eq≈ ? (join_comm ????));
   apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
 apply feq_plusr; apply plus_assoc;
 qed.
 
@@ -150,11 +150,11 @@ apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
   apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
-  apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
+  apply feq_plusl; apply (Eq≈ (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
     apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
   apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
-  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??));
+  repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∧x)∨y)) (eq_opp_opp_x_x ??));
   apply join_comm;]
 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
   apply eq_sym; apply plus_assoc;]
@@ -164,11 +164,11 @@ apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨
   repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
 apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????)));
+  apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∨z))) (eq_sym ??? (plus_assoc ????)));
   apply feq_plusl; apply plus_comm;]
 apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+  apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
   apply feq_plusl; apply plus_comm;]
 apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
@@ -200,11 +200,11 @@ apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
   apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
-  apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
+  apply feq_plusl; apply (Eq≈ (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
     apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
   apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
-  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??));
+  repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∨x)∧y)) (eq_opp_opp_x_x ??));
   apply meet_comm;]
 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
   apply eq_sym; apply plus_assoc;]
@@ -214,11 +214,11 @@ apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧
   repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
 apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????)));
+  apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∧z)))  (eq_sym ??? (plus_assoc ????)));
   apply feq_plusl; apply plus_comm;]
 apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+  repeat apply feq_plusr; apply (Eq≈ ?? (plus_assoc ????));
+  apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
   apply feq_plusl; apply plus_comm;]
 apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
   repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-- 
2.39.2