1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/ordered_divisible_group/".
17 include "nat/orders.ma".
18 include "nat/times.ma".
19 include "ordered_group.ma".
20 include "divisible_group.ma".
22 record todgroup : Type ≝ {
24 todg_division_: dgroup;
25 todg_with_: dg_carr todg_division_ = og_abelian_group todg_order
28 lemma todg_division: todgroup → dgroup.
29 intro G; apply (mk_dgroup G); unfold abelian_group_OF_todgroup;
30 cases (todg_with_ G); exact (dg_prop (todg_division_ G));
33 coercion cic:/matita/ordered_divisible_group/todg_division.con.
35 lemma pow_lt: ∀G:todgroup.∀x:G.∀n.0 < x → 0 < x + pow ? x n.
36 intros (G x n H); elim n; [
37 simplify; apply (lt_rewr ???? (plus_comm ???));
38 apply (lt_rewr ???x (zero_neutral ??)); assumption]
39 simplify; apply (lt_transitive ?? (x+(x)\sup(n1))); [assumption]
40 apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
41 apply (lt_rewl ??? (0 + (x \sup n1)) (eq_sym ??? (zero_neutral ??)));
42 apply (lt_rewl ???? (plus_comm ???));
43 apply flt_plusl; assumption;
46 lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ pow ? x n.
47 intros (G x n); elim n; simplify; [apply le_reflexive]
48 apply (le_transitive ???? H1);
49 apply (le_rewl ??? (0+(x\sup n1)) (zero_neutral ??));
50 apply fle_plusr; assumption;
53 lemma gt_pow: ∀G:todgroup.∀x:G.∀n.0 < pow ? x n → 0 < x.
55 simplify in l; cases (lt_coreflexive ?? l);]
57 cut (0+0<x+(x)\sup(n1));[2:
58 apply (lt_rewl ??? 0 (zero_neutral ??)); assumption].
59 cases (ltplus_orlt ????? Hcut); [assumption]
63 lemma gt_pow2: ∀G:dgroup.∀x,y:G.∀n.pow ? x n + pow ? y n ≈ pow ? (x+y) n.
64 intros (G x y n); elim n; [apply (Eq≈ 0 (zero_neutral ??)); apply eq_reflexive]
65 simplify; apply (Eq≈ (x+y+((x)\sup(n1)+(y)\sup(n1)))); [
66 apply (Eq≈ (x+((x)\sup(n1)+(y+(y)\sup(n1))))); [
67 apply eq_sym; apply plus_assoc;]
68 apply (Eq≈ (x+((x)\sup(n1)+y+(y)\sup(n1)))); [
69 apply feq_plusl; apply plus_assoc;]
70 apply (Eq≈ (x+(y+(x)\sup(n1)+(y)\sup(n1)))); [
71 apply feq_plusl; apply feq_plusr; apply plus_comm;]
72 apply (Eq≈ (x+(y+((x)\sup(n1)+(y)\sup(n1))))); [
73 apply feq_plusl; apply eq_sym; apply plus_assoc;]
75 apply feq_plusl; assumption;
78 lemma xxxx: ∀E:abelian_group.∀x,a,y,b:E.x + a # y + b → x # y ∨ a # b.
79 intros; cases (ap_cotransitive ??? (y+a) a1); [left|right]
80 [apply (plus_cancr_ap ??? a)|apply (plus_cancl_ap ??? y)]
84 lemma pow_gt0: ∀G:todgroup.∀y:G.∀n.0 < y → 0 < pow ? y (S n).
85 intros (G y n H); elim n; [apply (lt_rewr ??? (0+y) (plus_comm ???)); apply (lt_rewr ??? y (zero_neutral ??)); apply H]
86 simplify; apply (lt_rewl ? 0 ? (0+0) (zero_neutral ? 0));
87 apply ltplus; assumption;
90 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
91 intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
92 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
93 apply (gt_pow ?? (S (S n1))); apply (lt_rewr ???? f); assumption;
97 lemma bar1: ∀G:togroup.∀x,y:G.∀n.pow ? x (S n) # pow ? y (S n) → x # y.
98 intros 4 (G x y n); elim n; [2:
100 cases (xxxx ????? a); [assumption]
101 apply f; assumption;]
102 apply (plus_cancr_ap ??? 0); assumption;
106 lemma foo: ∀G:todgroup.∀x,y:G.∀n.
107 x < y → x\sup (S n) < y\sup (S n).
108 intros; elim n; [simplify; apply flt_plusr; assumption]
109 simplify; apply (ltplus); [assumption] assumption;
112 lemma foo1: ∀G:todgroup.∀x,y:G.∀n.
113 x\sup (S n) < y\sup (S n) → x < y.
114 intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
115 simplify in l; cases (ltplus_orlt ????? l); [assumption]
119 alias num (instance 0) = "natural number".
120 lemma foo3: ∀G:todgroup.∀x,y:G.
121 0<x → 0<y → x\sup 3 ≈ y\sup 4 → y < x.
122 intros (G x y H1 H2 H3); apply (foo1 ??? 2); apply (lt_rewr ???? H3);
123 simplify; repeat apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
124 apply (lt_rewr ???? (zero_neutral ??)); assumption;
127 alias num (instance 0) = "natural number".
128 lemma core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
129 intro G; cases G; unfold divide; intro e;
130 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
131 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
133 cut (0<w1\sup 3); [2: apply (lt_rewr ???? H2); assumption]
134 cut (0<w\sup 4); [2: apply (lt_rewr ???? H1); assumption]
135 lapply (gt_pow ??? Hcut) as H4;
136 lapply (gt_pow ??? Hcut1) as H5;
137 (* elim (eq_le_le ??? H1); elim (eq_le_le ??? H2); *)
138 cut (w<w1);[2: apply foo3; try assumption; apply (Eq≈ ? H2 H1);]
139 apply (plus_cancr_lt ??? w1);
140 apply (lt_rewl ??? (w+e)); [
141 apply (Eq≈ (w+w1\sup 3) ? H2);
142 apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
143 apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
144 simplify; repeat apply feq_plusl; apply eq_sym;
145 apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
146 apply (lt_rewl ???? (plus_comm ???));
147 apply flt_plusl; assumption;