1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
(* Example proof by Paul Roziere. See http://www.cs.kun.nl/~freek/comparison/ *)
Import nat.
flag auto_lvl 1.
theorem minimal.element /\X (\/n:N X n -> \/n:N (X n & /\p:N (X p -> n <= p))).
intro 2.
by_absurd.
rewrite_hyp H0 demorganl.
use /\n:N ~ X n.
trivial.
intros.
elim well_founded.N with H1.
intros.
intro.
apply H0 with H4.
lefts G $& $\/.
elim H3 with H5.
elim not.lesseq.imply.less.N.
save.
theorem not_odd_and_even.N /\x,y,z:N (~ (x = N2 * y & x = N1 + N2 * z)).
intro 2.
elim H.
trivial.
intros.
intro.
left H4.
elim H2 with [case].
trivial =H0 H4 H6.
elim H1.
axiom H3.
axiom H6.
intro.
rmh H4.
left H5.
intros.
rmh H5.
left H4.
axiom H4.
intros.
save.
theorem sum_square.N /\x,y:N (x + y)^N2 = x^N2 + N2*x*y + y^N2.
intros.
intro.
save.
fact less.exp.N /\n,x,y:N( x <= y -> x^n <= y^n).
intros.
elim H.
trivial.
rewrite calcul.N.
trivial.
save.
fact less_r.exp.N /\n,x,y:N( x^n < y^n -> x < y).
intros.
elim lesseq.case1.N with y and x.
apply less.exp.N with n and H3.
elim lesseq.imply.not.greater.N with y^n and x^n ;; Try intros.
save.
fact less.ladd.N /\x,y:N (N0 < y -> x < x + y).
intros.
elim H.
rewrite calcul.N.
trivial.
save.
theorem n.square.pair /\n:N (\/p:N n^N2=N2*p -> \/q:N n=N2*q).
intros.
lefts H0 $\/ $&.
apply odd_or_even.N with H.
lefts G $\/ $& $or.
trivial.
prove n^N2 = N1 + N2*(N2*y^N2+N2*y).
rewrite H3 sum_square.N.
from N1 + N2 * N2 * y + (N2 * y) ^ N2 = N1 + N4 * y + N2 * N2 * y ^ N2.
intro.
elim not_odd_and_even.N with N (n^N2).
intros.
select 3.
intro.
axiom H1.
axiom G.
axiom H0.
intros.
save.
lem decrease /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < n -> n < m).
intros.
elim less_r.exp.N with N2 ;; Try intros.
prove m^N2 = n^N2 + n^N2. axiom H1.
elim less.ladd.N ;; Try intros.
trivial =H0 H2.
save.
lem sup_zero /\m,n : N (m^ N2 = N2 * n^ N2 -> N0 < m -> N0 < n).
intros.
elim neq.less_or_sup.N with N0 and n ;; Try intros.
rewrite_hyp H1 H3 calcul.N.
trivial.
trivial.
save.
def Q m = m > N0 & \/n:N (m^ N2 = N2 * n^ N2).
lem dec /\m:N (Q m -> \/m':N (Q m' & m' < m)).
intros.
lefts H0 $Q $\/ $&.
apply sup_zero with H2 and H0.
intro.
instance ?1 n.
intros.
intros.
trivial.
prove \/p:N (m ^ N2 = N2 * p).
intro.
instance ?2 n^N2.
trivial.
apply n.square.pair with G0.
lefts G1 $& $\/.
prove n ^N2 = N2 * q ^N2.
rewrite_hyp H2 H4.
prove N2 * N2 * q ^N2 = N2 * n ^ N2.
from H2.
left G1.
trivial =.
intro.
intros.
intros.
intros.
trivial =H3 G1.
elim decrease.
save.
lem sq2_irrat /\m:N ~Q m.
intros.
intro.
elim minimal.element with Q.
intros $\/ $&.
axiom H.
axiom H0.
lefts H1.
elim dec with H2.
lefts H4.
apply H3 with H5.
elim lesseq.imply.not.greater.N with n and m'.
save.
theorem square2_irrat /\m,n : N (m^ N2 = N2 * n^ N2 -> m = N0 & n = N0).
intros.
apply sq2_irrat with H.
elim H with [case].
intro.
intro.
elim H0 with [case].
intro.
rewrite_hyp H1 H2 H4 calcul.N.
left H1;; intros.
prove Q m.
intros $Q $\/ $& ;; Try axiom H1.
trivial.
elim G.
save.
|
