From 2030804124914a9b2155c911d4b835fd67c26d4e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Nov 2007 09:11:48 +0000 Subject: [PATCH] snapshot --- matita/dama/excedence.ma | 5 +---- matita/dama/groups.ma | 22 ++++++---------------- matita/dama/ordered_groups.ma | 15 ++++++++++++++- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma index d91c61170..6d1fc4dd7 100644 --- a/matita/dama/excedence.ma +++ b/matita/dama/excedence.ma @@ -104,8 +104,7 @@ lemma lt_coreflexive: ∀E.coreflexive ? (lt E). intros 2 (E x); intro H; cases H (_ ABS); apply (ap_coreflexive ? x ABS); qed. - -(* + lemma lt_transitive: ∀E.transitive ? (lt E). intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2; @@ -120,5 +119,3 @@ theorem lt_to_excede: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a). intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *) qed. - -*) \ No newline at end of file diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma index 3e30e0474..da24dadc5 100644 --- a/matita/dama/groups.ma +++ b/matita/dama/groups.ma @@ -149,22 +149,12 @@ qed. theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x. intros (G x); apply (plus_cancl ??? (-x)); apply (eq_transitive ?? (--x + -x)); [apply plus_comm] -apply (eq_transitive (carr G) (plus G (opp G (opp G x)) (opp G x)) (zero G) (plus G (opp G x) x) ? ?); - [apply (opp_inverse G (opp G x)). - |apply (eq_symmetric (carr G) (plus G (opp G x) x) (zero G) ?). - apply (opp_inverse G x). - ] +apply (eq_transitive ?? 0); [apply opp_inverse] +apply eq_symmetric; apply opp_inverse; qed. -theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. - [ assumption - | intros; -apply (eq_transitive (carr G) (zero G) (plus G (opp G (zero G)) (zero G)) (opp G (zero G)) ? ?); - [apply (eq_symmetric (carr G) (plus G (opp G (zero G)) (zero G)) (zero G) ?). - apply (opp_inverse G (zero G)). - |apply (eq_transitive (carr G) (plus G (opp G (zero G)) (zero G)) (plus G (zero G) (opp G (zero G))) (opp G (zero G)) ? ?); - [apply (plus_comm G (opp G (zero G)) (zero G)). - |apply (zero_neutral G (opp G (zero G))). - ] - ]] +theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption] +intro G; apply (plus_cancr ??? 0); +apply (eq_transitive ?? 0); [apply zero_neutral;] +apply eq_symmetric; apply opp_inverse; qed. diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma index 4d2e18e28..9e72cab59 100644 --- a/matita/dama/ordered_groups.ma +++ b/matita/dama/ordered_groups.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/ordered_groups/". -include "groups.ma". include "ordered_sets.ma". +include "groups.ma". record pre_ordered_abelian_group : Type ≝ { og_abelian_group_: abelian_group; @@ -41,6 +41,19 @@ record ordered_abelian_group : Type ≝ is_ordered_abelian_group og_pre_ordered_abelian_group }. +lemma le_rewl: ∀E:excedence.∀x,z,y:E. x ≈ y → x ≤ z → y ≤ z. +intros (E x z y); apply (le_transitive ???? ? H1); +clear H1 z; unfold in H; unfold; intro H1; apply H; clear H; +lapply ap_cotransitive; +intros (G x z y); intro Eyz; + + +lemma plus_cancr_le: + ∀G:ordered_abelian_group.∀x,y,z:G.x+z ≤ y + z → x ≤ y. +intros 5 (G x y z L); + + apply L; clear L; elim (exc_cotransitive ???z Exy); + lemma le_zero_x_to_le_opp_x_zero: ∀G:ordered_abelian_group.∀x:G.0 ≤ x → -x ≤ 0. intros (G x Px); -- 2.39.2