From 46fb7c601185d7aada2489700e7d7817d50e1e57 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Jan 2008 15:37:11 +0000 Subject: [PATCH] many sed to use notation for rewriting --- helm/software/matita/dama/depends | 10 +- helm/software/matita/dama/divisible_group.ma | 4 +- helm/software/matita/dama/excess.ma | 17 +- helm/software/matita/dama/group.ma | 35 ++-- .../matita/dama/ordered_divisible_group.ma | 18 +-- helm/software/matita/dama/ordered_group.ma | 152 +++++++++--------- 6 files changed, 120 insertions(+), 116 deletions(-) diff --git a/helm/software/matita/dama/depends b/helm/software/matita/dama/depends index a047fc9d1..1fe102822 100644 --- a/helm/software/matita/dama/depends +++ b/helm/software/matita/dama/depends @@ -25,16 +25,10 @@ attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma attic/vector_spaces.ma attic/reals.ma attic/rings.ma group.ma attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma -nat/nat.ma -logic/connectives.ma -higher_order_defs/relations.ma Q/q.ma -nat/plus.ma higher_order_defs/relations.ma logic/connectives.ma -nat/orders.ma -nat/times.ma -nat/orders.ma +nat/nat.ma nat/orders.ma nat/plus.ma -nat/orders.ma +nat/times.ma diff --git a/helm/software/matita/dama/divisible_group.ma b/helm/software/matita/dama/divisible_group.ma index 4f54545c8..3a79b11bb 100644 --- a/helm/software/matita/dama/divisible_group.ma +++ b/helm/software/matita/dama/divisible_group.ma @@ -50,8 +50,8 @@ qed. lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x. intro G; cases G; unfold divide; intros; simplify; cases (f x O); simplify; simplify in H; intro; apply H; -apply (ap_rewl ???? (plus_comm ???)); -apply (ap_rewl ???w (zero_neutral ??)); assumption; +apply (Ap≪ ? (plus_comm ???)); +apply (Ap≪ w (zero_neutral ??)); assumption; qed. lemma apmul_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y. diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma index 6db7e22e6..c7d31c229 100644 --- a/helm/software/matita/dama/excess.ma +++ b/helm/software/matita/dama/excess.ma @@ -173,6 +173,18 @@ intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); apply ap_symmetric; assumption; qed. +notation > "'Ap'≪" non associative with precedence 50 for + @{'aprewritel}. + +interpretation "ap_rewl" 'aprewritel = + (cic:/matita/excess/ap_rewl.con _ _ _). + +notation > "'Ap'≫" non associative with precedence 50 for + @{'aprewriter}. + +interpretation "ap_rewr" 'aprewriter = + (cic:/matita/excess/ap_rewr.con _ _ _). + lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption] cases Exy; right; assumption; @@ -197,12 +209,12 @@ interpretation "exc_rewr" 'excessrewriter = lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. intros (A x y z E H); split; elim H; -[apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption; +[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption; qed. lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z. intros (A x y z E H); split; elim H; -[apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption; +[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption; qed. notation > "'Lt'≪" non associative with precedence 50 for @@ -246,4 +258,3 @@ qed. definition total_order_property : ∀E:excess. Type ≝ λE:excess. ∀a,b:E. a ≰ b → b < a. - diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma index 9da386ef7..104dcf274 100644 --- a/helm/software/matita/dama/group.ma +++ b/helm/software/matita/dama/group.ma @@ -80,7 +80,7 @@ coercion cic:/matita/group/feq_plusl.con nocomposites. lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z). intros 5 (G z x y A); simplify in A; lapply (plus_comm ? z x) as E1; lapply (plus_comm ? z y) as E2; -lapply (ap_rewl ???? E1 A) as A1; lapply (ap_rewr ???? E2 A1) as A2; +lapply (Ap≪ ? E1 A) as A1; lapply (Ap≫ ? E2 A1) as A2; apply (plus_strong_ext ???? A2); qed. @@ -111,31 +111,31 @@ coercion cic:/matita/group/feq_plusl_sym_.con nocomposites. lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z. intros (G x y z Ayz); apply (plus_strong_ext ? (-x)); -apply (ap_rewl ??? ((-x + x) + y)); +apply (Ap≪ ((-x + x) + y)); [1: apply plus_assoc; -|2: apply (ap_rewr ??? ((-x +x) +z)); +|2: apply (Ap≫ ((-x +x) +z)); [1: apply plus_assoc; - |2: apply (ap_rewl ??? (0 + y)); + |2: apply (Ap≪ (0 + y)); [1: apply (feq_plusr ???? (opp_inverse ??)); - |2: apply (ap_rewl ???? (zero_neutral ? y)); - apply (ap_rewr ??? (0 + z) (opp_inverse ??)); - apply (ap_rewr ???? (zero_neutral ??)); assumption;]]] + |2: apply (Ap≪ ? (zero_neutral ? y)); + apply (Ap≫ (0 + z) (opp_inverse ??)); + apply (Ap≫ ? (zero_neutral ??)); assumption;]]] qed. lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x. intros (G x y z Ayz); apply (plus_strong_extr ? (-x)); -apply (ap_rewl ??? (y + (x + -x))); +apply (Ap≪ (y + (x + -x))); [1: apply (eq_sym ??? (plus_assoc ????)); -|2: apply (ap_rewr ??? (z + (x + -x))); +|2: apply (Ap≫ (z + (x + -x))); [1: apply (eq_sym ??? (plus_assoc ????)); - |2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x))); - apply (ap_rewl ??? (y + 0) (opp_inverse ??)); - apply (ap_rewl ??? (0 + y) (plus_comm ???)); - apply (ap_rewl ??? y (zero_neutral ??)); - apply (ap_rewr ??? (z + (-x+x)) (plus_comm ? x (-x))); - apply (ap_rewr ??? (z + 0) (opp_inverse ??)); - apply (ap_rewr ??? (0 + z) (plus_comm ???)); - apply (ap_rewr ??? z (zero_neutral ??)); + |2: apply (Ap≪ (y + (-x+x)) (plus_comm ? x (-x))); + apply (Ap≪ (y + 0) (opp_inverse ??)); + apply (Ap≪ (0 + y) (plus_comm ???)); + apply (Ap≪ y (zero_neutral ??)); + apply (Ap≫ (z + (-x+x)) (plus_comm ? x (-x))); + apply (Ap≫ (z + 0) (opp_inverse ??)); + apply (Ap≫ (0 + z) (plus_comm ???)); + apply (Ap≫ z (zero_neutral ??)); assumption]] qed. @@ -183,7 +183,6 @@ 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 ??)); *) apply (Eq≈ 0 ? (opp_inverse ??)); apply (Eq≈ (-y + z) H2); apply (Eq≈ (-y + y) H1); diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma index a9671d934..15dd52cdb 100644 --- a/helm/software/matita/dama/ordered_divisible_group.ma +++ b/helm/software/matita/dama/ordered_divisible_group.ma @@ -35,7 +35,7 @@ coercion cic:/matita/ordered_divisible_group/todg_division.con. lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x. intros (G x n); elim n; simplify; [apply le_reflexive] apply (le_transitive ???? H1); -apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??)); +apply (Le≪ (0+(n1*x)) (zero_neutral ??)); apply fle_plusr; assumption; qed. @@ -51,25 +51,25 @@ apply f; assumption; qed. lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0 sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [ + rewrite > sym_plus; simplify; apply (Lt≪ (0+(y+n*y))); [ apply eq_sym; apply zero_neutral] apply flt_plusr; assumption;] apply (lt_transitive ???? l); rewrite > sym_plus; simplify; rewrite > (sym_plus n); simplify; repeat apply flt_plusl; -apply (lt_rewl ???(0+(n1+n)*y)); [apply eq_sym; apply zero_neutral] +apply (Lt≪ (0+(n1+n)*y)); [apply eq_sym; apply zero_neutral] apply flt_plusr; assumption; qed. diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma index 9a066a80e..8677e755b 100644 --- a/helm/software/matita/dama/ordered_group.ma +++ b/helm/software/matita/dama/ordered_group.ma @@ -55,19 +55,19 @@ coercion cic:/matita/ordered_group/fexc_plusr.con nocomposites. lemma plus_cancl_exc: ∀G:pogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. intros 5 (G x y z L); apply (plus_cancr_exc ??? z); -apply (exc_rewl ??? (z+x) (plus_comm ???)); -apply (exc_rewr ??? (z+y) (plus_comm ???) L); +apply (Ex≪ (z+x) (plus_comm ???)); +apply (Ex≫ (z+y) (plus_comm ???) L); qed. lemma fexc_plusl: ∀G:pogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y. intros 5 (G x y z L); apply (plus_cancl_exc ??? (-z)); -apply (exc_rewl ???? (plus_assoc ??z x)); -apply (exc_rewr ???? (plus_assoc ??z y)); -apply (exc_rewl ??? (0+x) (opp_inverse ??)); -apply (exc_rewr ??? (0+y) (opp_inverse ??)); -apply (exc_rewl ???? (zero_neutral ??)); -apply (exc_rewr ???? (zero_neutral ??) L); +apply (Ex≪? (plus_assoc ??z x)); +apply (Ex≫? (plus_assoc ??z y)); +apply (Ex≪ (0+x) (opp_inverse ??)); +apply (Ex≫ (0+y) (opp_inverse ??)); +apply (Ex≪? (zero_neutral ??)); +apply (Ex≫? (zero_neutral ??) L); qed. coercion cic:/matita/ordered_group/fexc_plusl.con nocomposites. @@ -75,50 +75,50 @@ coercion cic:/matita/ordered_group/fexc_plusl.con nocomposites. lemma plus_cancr_le: ∀G:pogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. intros 5 (G x y z L); -apply (le_rewl ??? (0+x) (zero_neutral ??)); -apply (le_rewl ??? (x+0) (plus_comm ???)); -apply (le_rewl ??? (x+(-z+z)) (opp_inverse ??)); -apply (le_rewl ??? (x+(z+ -z)) (plus_comm ??z)); -apply (le_rewl ??? (x+z+ -z) (plus_assoc ????)); -apply (le_rewr ??? (0+y) (zero_neutral ??)); -apply (le_rewr ??? (y+0) (plus_comm ???)); -apply (le_rewr ??? (y+(-z+z)) (opp_inverse ??)); -apply (le_rewr ??? (y+(z+ -z)) (plus_comm ??z)); -apply (le_rewr ??? (y+z+ -z) (plus_assoc ????)); +apply (Le≪ (0+x) (zero_neutral ??)); +apply (Le≪ (x+0) (plus_comm ???)); +apply (Le≪ (x+(-z+z)) (opp_inverse ??)); +apply (Le≪ (x+(z+ -z)) (plus_comm ??z)); +apply (Le≪ (x+z+ -z) (plus_assoc ????)); +apply (Le≫ (0+y) (zero_neutral ??)); +apply (Le≫ (y+0) (plus_comm ???)); +apply (Le≫ (y+(-z+z)) (opp_inverse ??)); +apply (Le≫ (y+(z+ -z)) (plus_comm ??z)); +apply (Le≫ (y+z+ -z) (plus_assoc ????)); intro H; apply L; clear L; apply (plus_cancr_exc ??? (-z) H); qed. lemma fle_plusl: ∀G:pogroup. ∀f,g,h:G. f≤g → h+f≤h+g. intros (G f g h); apply (plus_cancr_le ??? (-h)); -apply (le_rewl ??? (f+h+ -h) (plus_comm ? f h)); -apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????)); -apply (le_rewl ??? (f+(-h+h)) (plus_comm ? h (-h))); -apply (le_rewl ??? (f+0) (opp_inverse ??)); -apply (le_rewl ??? (0+f) (plus_comm ???)); -apply (le_rewl ??? (f) (zero_neutral ??)); -apply (le_rewr ??? (g+h+ -h) (plus_comm ? h ?)); -apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????)); -apply (le_rewr ??? (g+(-h+h)) (plus_comm ??h)); -apply (le_rewr ??? (g+0) (opp_inverse ??)); -apply (le_rewr ??? (0+g) (plus_comm ???)); -apply (le_rewr ??? (g) (zero_neutral ??) H); +apply (Le≪ (f+h+ -h) (plus_comm ? f h)); +apply (Le≪ (f+(h+ -h)) (plus_assoc ????)); +apply (Le≪ (f+(-h+h)) (plus_comm ? h (-h))); +apply (Le≪ (f+0) (opp_inverse ??)); +apply (Le≪ (0+f) (plus_comm ???)); +apply (Le≪ (f) (zero_neutral ??)); +apply (Le≫ (g+h+ -h) (plus_comm ? h ?)); +apply (Le≫ (g+(h+ -h)) (plus_assoc ????)); +apply (Le≫ (g+(-h+h)) (plus_comm ??h)); +apply (Le≫ (g+0) (opp_inverse ??)); +apply (Le≫ (0+g) (plus_comm ???)); +apply (Le≫ (g) (zero_neutral ??) H); qed. lemma fle_plusr: ∀G:pogroup. ∀f,g,h:G. f≤g → f+h≤g+h. -intros (G f g h H); apply (le_rewl ???? (plus_comm ???)); -apply (le_rewr ???? (plus_comm ???)); apply fle_plusl; assumption; +intros (G f g h H); apply (Le≪? (plus_comm ???)); +apply (Le≫? (plus_comm ???)); apply fle_plusl; assumption; qed. lemma plus_cancl_le: ∀G:pogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y. intros 5 (G x y z L); -apply (le_rewl ??? (0+x) (zero_neutral ??)); -apply (le_rewl ??? ((-z+z)+x) (opp_inverse ??)); -apply (le_rewl ??? (-z+(z+x)) (plus_assoc ????)); -apply (le_rewr ??? (0+y) (zero_neutral ??)); -apply (le_rewr ??? ((-z+z)+y) (opp_inverse ??)); -apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????)); +apply (Le≪ (0+x) (zero_neutral ??)); +apply (Le≪ ((-z+z)+x) (opp_inverse ??)); +apply (Le≪ (-z+(z+x)) (plus_assoc ????)); +apply (Le≫ (0+y) (zero_neutral ??)); +apply (Le≫ ((-z+z)+y) (opp_inverse ??)); +apply (Le≫ (-z+(z+y)) (plus_assoc ????)); apply (fle_plusl ??? (-z) L); qed. @@ -138,55 +138,55 @@ qed. lemma exc_opp_x_zero_to_exc_zero_x: ∀G:pogroup.∀x:G.-x ≰ 0 → 0 ≰ x. intros (G x H); apply (plus_cancr_exc ??? (-x)); -apply (exc_rewr ???? (plus_comm ???)); -apply (exc_rewr ???? (opp_inverse ??)); -apply (exc_rewl ???? (zero_neutral ??) H); +apply (Ex≫? (plus_comm ???)); +apply (Ex≫? (opp_inverse ??)); +apply (Ex≪? (zero_neutral ??) H); qed. lemma le_zero_x_to_le_opp_x_zero: ∀G:pogroup.∀x:G.0 ≤ x → -x ≤ 0. intros (G x Px); apply (plus_cancr_le ??? x); -apply (le_rewl ??? 0 (opp_inverse ??)); -apply (le_rewr ??? x (zero_neutral ??) Px); +apply (Le≪ 0 (opp_inverse ??)); +apply (Le≫ x (zero_neutral ??) Px); qed. lemma lt_zero_x_to_lt_opp_x_zero: ∀G:pogroup.∀x:G.0 < x → -x < 0. intros (G x Px); apply (plus_cancr_lt ??? x); -apply (lt_rewl ??? 0 (opp_inverse ??)); -apply (lt_rewr ??? x (zero_neutral ??) Px); +apply (Lt≪ 0 (opp_inverse ??)); +apply (Lt≫ x (zero_neutral ??) Px); qed. lemma exc_zero_opp_x_to_exc_x_zero: ∀G:pogroup.∀x:G. 0 ≰ -x → x ≰ 0. intros (G x H); apply (plus_cancl_exc ??? (-x)); -apply (exc_rewr ???? (plus_comm ???)); -apply (exc_rewl ???? (opp_inverse ??)); -apply (exc_rewr ???? (zero_neutral ??) H); +apply (Ex≫? (plus_comm ???)); +apply (Ex≪? (opp_inverse ??)); +apply (Ex≫? (zero_neutral ??) H); qed. lemma le_x_zero_to_le_zero_opp_x: ∀G:pogroup.∀x:G. x ≤ 0 → 0 ≤ -x. intros (G x Lx0); apply (plus_cancr_le ??? x); -apply (le_rewr ??? 0 (opp_inverse ??)); -apply (le_rewl ??? x (zero_neutral ??)); +apply (Le≫ 0 (opp_inverse ??)); +apply (Le≪ x (zero_neutral ??)); assumption; qed. lemma lt_x_zero_to_lt_zero_opp_x: ∀G:pogroup.∀x:G. x < 0 → 0 < -x. intros (G x Lx0); apply (plus_cancr_lt ??? x); -apply (lt_rewr ??? 0 (opp_inverse ??)); -apply (lt_rewl ??? x (zero_neutral ??)); +apply (Lt≫ 0 (opp_inverse ??)); +apply (Lt≪ x (zero_neutral ??)); assumption; qed. lemma lt_opp_x_zero_to_lt_zero_x: ∀G:pogroup.∀x:G. -x < 0 → 0 < x. intros (G x Lx0); apply (plus_cancr_lt ??? (-x)); -apply (lt_rewl ??? (-x) (zero_neutral ??)); -apply (lt_rewr ??? (-x+x) (plus_comm ???)); -apply (lt_rewr ??? 0 (opp_inverse ??)); +apply (Lt≪ (-x) (zero_neutral ??)); +apply (Lt≫ (-x+x) (plus_comm ???)); +apply (Lt≫ 0 (opp_inverse ??)); assumption; qed. @@ -194,7 +194,7 @@ lemma lt0plus_orlt: ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y. intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2); [right; split; assumption|left;split;[assumption]] -apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??)); +apply (plus_cancr_ap ??? y); apply (Ap≪? (zero_neutral ??)); assumption; qed. @@ -202,10 +202,10 @@ lemma le0plus_le: ∀G:pogroup.∀a,b,c:G. 0 ≤ b → a + b ≤ c → a ≤ c. intros (G a b c L H); apply (le_transitive ????? H); apply (plus_cancl_le ??? (-a)); -apply (le_rewl ??? 0 (opp_inverse ??)); -apply (le_rewr ??? (-a + a + b) (plus_assoc ????)); -apply (le_rewr ??? (0 + b) (opp_inverse ??)); -apply (le_rewr ??? b (zero_neutral ??)); +apply (Le≪ 0 (opp_inverse ??)); +apply (Le≫ (-a + a + b) (plus_assoc ????)); +apply (Le≫ (0 + b) (opp_inverse ??)); +apply (Le≫ b (zero_neutral ??)); assumption; qed. @@ -213,10 +213,10 @@ lemma le_le0plus: ∀G:pogroup.∀a,b:G. 0 ≤ a → 0 ≤ b → 0 ≤ a + b. intros (G a b L1 L2); apply (le_transitive ???? L1); apply (plus_cancl_le ??? (-a)); -apply (le_rewl ??? 0 (opp_inverse ??)); -apply (le_rewr ??? (-a + a + b) (plus_assoc ????)); -apply (le_rewr ??? (0 + b) (opp_inverse ??)); -apply (le_rewr ??? b (zero_neutral ??)); +apply (Le≪ 0 (opp_inverse ??)); +apply (Le≫ (-a + a + b) (plus_assoc ????)); +apply (Le≫ (0 + b) (opp_inverse ??)); +apply (Le≫ b (zero_neutral ??)); assumption; qed. @@ -235,8 +235,8 @@ qed. lemma ltxy_ltyyxx: ∀G:pogroup.∀x,y:G. y < x → y+y < x+x. intros; apply (lt_transitive ?? (y+x));[2: - apply (lt_rewl ???? (plus_comm ???)); - apply (lt_rewr ???? (plus_comm ???));] + apply (Lt≪? (plus_comm ???)); + apply (Lt≫? (plus_comm ???));] apply flt_plusl;assumption; qed. @@ -244,10 +244,10 @@ lemma lew_opp : ∀O:pogroup.∀a,b,c:O.0 ≤ b → a ≤ c → a + -b ≤ c. intros (O a b c L0 L); apply (le_transitive ????? L); apply (plus_cancl_le ??? (-a)); -apply (le_rewr ??? 0 (opp_inverse ??)); -apply (le_rewl ??? (-a+a+-b) (plus_assoc ????)); -apply (le_rewl ??? (0+-b) (opp_inverse ??)); -apply (le_rewl ??? (-b) (zero_neutral ?(-b))); +apply (Le≫ 0 (opp_inverse ??)); +apply (Le≪ (-a+a+-b) (plus_assoc ????)); +apply (Le≪ (0+-b) (opp_inverse ??)); +apply (Le≪ (-b) (zero_neutral ?(-b))); apply le_zero_x_to_le_opp_x_zero; assumption; qed. @@ -256,10 +256,10 @@ lemma ltw_opp : ∀O:pogroup.∀a,b,c:O.0 < b → a < c → a + -b < c. intros (O a b c P L); apply (lt_transitive ????? L); apply (plus_cancl_lt ??? (-a)); -apply (lt_rewr ??? 0 (opp_inverse ??)); -apply (lt_rewl ??? (-a+a+-b) (plus_assoc ????)); -apply (lt_rewl ??? (0+-b) (opp_inverse ??)); -apply (lt_rewl ??? ? (zero_neutral ??)); +apply (Lt≫ 0 (opp_inverse ??)); +apply (Lt≪ (-a+a+-b) (plus_assoc ????)); +apply (Lt≪ (0+-b) (opp_inverse ??)); +apply (Lt≪ ? (zero_neutral ??)); apply lt_zero_x_to_lt_opp_x_zero; assumption; qed. @@ -282,7 +282,7 @@ qed. lemma applus_orap: ∀G:abelian_group. ∀x,y:G. 0 # x + y → 0 #x ∨ 0#y. intros; cases (ap_cotransitive ??? y a); [right; assumption] -left; apply (plus_cancr_ap ??? y); apply (ap_rewl ???y (zero_neutral ??)); +left; apply (plus_cancr_ap ??? y); apply (Ap≪y (zero_neutral ??)); assumption; qed. @@ -310,7 +310,7 @@ intros; intro; apply H; lapply (lt_to_excess ??? l); lapply (tog_total ??? e); lapply (tog_total ??? Hletin); lapply (ltplus ????? Hletin2 Hletin1); -apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral] +apply (Ex≪ (0+0)); [apply eq_sym; apply zero_neutral] apply lt_to_excess; assumption; qed. -- 2.39.2