# source:Deliverables/D4.1/Matita/Nat.ma@363

Last change on this file since 363 was 363, checked in by mulligan, 10 years ago

Resolved conflicts. Added new get_index' which hides the proof obligation of get_index_v. Needed a new lemma to typecheck it.

File size: 17.8 KB
Line
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4include "Cartesian.ma".
5include "Bool.ma".
6include "Connectives.ma".
7
8(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
9(* The datatype.                                                              *)
10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11ninductive Nat: Type[0] ≝
12  Z: Nat
13| S: Nat → Nat.
14
15ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m.
16 #n m H;
17 nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]);
18 napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]);
19 nnormalize; /3/.
20nqed.
21
22(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
23(* Orderings.                                                                 *)
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25
26ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
27  ltoe_refl: less_than_or_equal_p n n
28| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).
29
30nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
31  match m with
32    [ Z ⇒ true
33    | S o ⇒
34      match n with
35        [ Z ⇒ false
36        | S p ⇒ less_than_or_equal_b o p
37        ]
38    ].
39
40notation "hvbox(n break ≤ m)"
41  non associative with precedence 47
42  for @{ 'less_than_or_equal \$n \$m }.
43
44interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
45
46notation "hvbox(n break ≲ m)"
47  non associative with precedence 47
48  for @{ 'less_than_or_equalb \$n \$m }.
49
50interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m).
51
52
53ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
54  λm, n: Nat.
55    n ≤ m.
56
57ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
58  λm, n: Nat.
59    less_than_or_equal_b n m.
60
61notation "hvbox(n break ≥ m)"
62  non associative with precedence 47
63  for @{ 'greater_than_or_equal \$n \$m }.
64
65
66interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
67
68notation "hvbox(n break ≳ m)"
69  non associative with precedence 47
70  for @{ 'greater_than_or_equalb \$n \$m }.
71
72interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m).
73
74
76ndefinition less_than_p ≝
77  λm: Nat.
78  λn: Nat.
79    less_than_or_equal_p (S m) n.
80
81notation "hvbox(n break < m)"
82  non associative with precedence 47
83  for @{ 'less_than \$n \$m }.
84
85interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).
86
87ndefinition greater_than_p ≝
88  λm, n: Nat.
89    n < m.
90
91notation "hvbox(n break > m)"
92  non associative with precedence 47
93  for @{ 'greater_than \$n \$m }.
94
95interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
96
97nlet rec less_than_b (m: Nat) (n: Nat) on m ≝
98  match m with
99    [ Z ⇒
100      match n with
101        [ Z ⇒ false
102        | S o ⇒ true
103        ]
104    | S o ⇒
105      match n with
106        [ Z ⇒ false
107        | S p ⇒ less_than_b o p
108        ]
109    ].
110
111(* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *)
112
113ndefinition greater_than_b ≝
114  λm, n: Nat.
115    less_than_b n m.
116
117(* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *)
118
119(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
121(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
122nlet rec plus (n: Nat) (o: Nat) on n ≝
123  match n with
124    [ Z ⇒ o
125    | S p ⇒ S (plus p o)
126    ].
127
128notation "hvbox(n break + m)"
129  right associative with precedence 52
130  for @{ 'plus \$n \$m }.
131
132interpretation "Nat plus" 'plus n m = (plus n m).
133
134nlet rec minus (n: Nat) (o: Nat) on n ≝
135  match n with
136    [ Z ⇒ Z
137    | S p ⇒
138      match o with
139        [ Z ⇒ S p
140        | S q ⇒ minus p q
141        ]
142    ].
143
144notation "hvbox(n break - m)"
145  right associative with precedence 47
146  for @{ 'minus \$n \$m }.
147
148interpretation "Nat minus" 'minus n m = (minus n m).
149
150(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
151(* Multiplication, modulus and division.                                      *)
152(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
153
154nlet rec multiplication (n: Nat) (o: Nat) on n ≝
155  match n with
156    [ Z ⇒ Z
157    | S p ⇒ o + (multiplication p o)
158    ].
159
160notation "hvbox(n break * m)"
161  right associative with precedence 47
162  for @{ 'multiplication \$n \$m }.
163
164interpretation "Nat multiplication" 'times n m = (multiplication n m).
165
166nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
167  match less_than_or_equal_b n p with
168    [ true ⇒ Z
169    | false ⇒
170      match m with
171        [ Z ⇒ Z
172        | (S q) ⇒ S (division_aux q (n - (S p)) p)
173        ]
174    ].
175
176ndefinition division ≝
177  λm, n: Nat.
178    match n with
179      [ Z ⇒ S m
180      | S o ⇒ division_aux m m o
181      ].
182
183notation "hvbox(n break ÷ m)"
184  right associative with precedence 47
185  for @{ 'division \$n \$m }.
186
187interpretation "Nat division" 'division n m = (division n m).
188
189nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
190  match less_than_or_equal_b n p with
191    [ true ⇒ n
192    | false ⇒
193      match m with
194        [ Z ⇒ n
195        | S o ⇒ modulus_aux o (n - (S p)) p
196        ]
197    ].
198
199ndefinition modulus ≝
200  λm, n: Nat.
201    match n with
202      [ Z ⇒ m
203      | S o ⇒ modulus_aux m m o
204      ].
205
206notation "hvbox(n break 'mod' m)"
207  right associative with precedence 47
208  for @{ 'modulus \$n \$m }.
209
210interpretation "Nat modulus" 'modulus m n = (modulus m n).
211
212ndefinition divide_with_remainder ≝
213  λm, n: Nat.
214    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
215
216(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
217(* Exponentials, and square roots.                                            *)
218(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
219
220nlet rec exponential (m: Nat) (n: Nat) on n ≝
221  match n with
222    [ Z ⇒ S (Z)
223    | S o ⇒ m * exponential m o
224    ].
225
226notation "hvbox(n ^ m)"
227  left associative with precedence 52
228  for @{ 'exponential \$n \$m }.
229
230interpretation "Nat exponential" 'exponential n m = (exponential n m).
231
232nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝
233  match m with
234    [ Z ⇒
235      match n with
236        [ Z ⇒ true
237        | _ ⇒ false
238        ]
239    | S o ⇒
240      match n with
241        [ S p ⇒ eq_n o p
242        | _ ⇒ false
243        ]
244    ].
245
246(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
247(* Greatest common divisor and least common multiple.                         *)
248(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
249
250(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
251(* Axioms.                                                                    *)
252(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
253
254(*naxiom plus_minus_inverse_left:
255  ∀m, n: Nat.
256    (m + n) - n = m.
257*)
258
259ntheorem less_than_or_equal_monotone:
260  ∀m, n: Nat.
261    m ≤ n → (S m) ≤ (S n).
262 #m n H; nelim H; /2/.
263nqed.
264
265nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l.
266 #n m l H H1; nelim H1; /2/.
267nqed.
268
269ntheorem less_than_or_equal_injective:
270  ∀m, n: Nat.
271    (S m) ≤ (S n) → m ≤ n.
272 #m n H;
273 nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]);
274 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]);
275 nnormalize; /3/.
276nqed.
277
278ntheorem succ_less_than_injective:
279  ∀m, n: Nat.
280    less_than_p (S m) (S n) → m < n.
281 /2/.
282nqed.
283
284nlemma not_less_than_S_Z:
285 ∀m,n: Nat. S m ≤ n → ¬ (n = Z).
286 #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ]
287nqed.
288
289ntheorem nothing_less_than_Z:
290  ∀m: Nat.
291    ¬(m < Z).
292 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
293nqed.
294
295
296(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
297(* Lemmas.                                                                    *)
298(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
299
300nlemma less_than_or_equal_zero:
301  ∀n: Nat.
302    Z ≤ n.
303  #n.
304  nelim n.
305  //.
306  #N.
307  napply ltoe_step.
308nqed.
309
310(*
311nlemma less_than_or_equal_zero_equal_zero:
312  ∀m: Nat.
313    m ≤ Z → m = Z.
314  #m.
315  nelim m.
316  //.
317  #N H H2.
318  nnormalize.
319*)
320
321nlemma less_than_or_equal_reflexive:
322  ∀n: Nat.
323    n ≤ n.
324  #n.
325  nelim n.
326  nnormalize.
327  @.
328  #N H.
329  nnormalize.
330  //.
331nqed.
332
333(*
334nlemma less_than_or_equal_succ:
335  ∀m, n: Nat.
336    S m ≤ n → m ≤ n.
337  #m n.
338  nelim m.
339  #H.
340  napplyS less_than_or_equal_zero.
341  #N H H2.
342  nrewrite > H.
343  nnormalize.
344
345nlemma less_than_or_equal_transitive:
346  ∀m, n, o: Nat.
347    m ≤ n ∧ n ≤ o → m ≤ o.
348  #m n o.
349  nelim m.
350  #H.
351  napply less_than_or_equal_zero.
352  #N H H2.
353  nnormalize.
354*)
355
356nlemma plus_zero:
357  ∀n: Nat.
358    n + Z = n.
359  #n.
360  nelim n.
361  nnormalize.
362  @.
363  #N H.
364  nnormalize.
365  nrewrite > H.
366  @.
367nqed.
368
369nlemma plus_associative:
370  ∀m, n, o: Nat.
371    (m + n) + o = m + (n + o).
372  #m n o.
373  nelim m.
374  nnormalize.
375  @.
376  #N H.
377  nnormalize.
378  nrewrite > H.
379  @.
380nqed.
381
382nlemma succ_plus:
383  ∀m, n: Nat.
384    S(m + n) = m + S(n).
385  #m n.
386  nelim m.
387  nnormalize.
388  @.
389  #N H.
390  nnormalize.
391  nrewrite > H.
392  @.
393nqed.
394
395nlemma succ_plus_succ_zero:
396  ∀n: Nat.
397    S n = plus n (S Z).
398  #n.
399  nelim n.
400  //.
401  #N H.
402  nnormalize.
403  nrewrite < H.
404  @.
405nqed.
406
407nlemma plus_symmetrical:
408  ∀m, n: Nat.
409    m + n = n + m.
410  #m n.
411  nelim m.
412  nnormalize.
413  nelim n.
414  nnormalize.
415  @.
416  #N H.
417  nnormalize.
418  nrewrite < H.
419  @.
420  #N H.
421  nnormalize.
422  nrewrite > H.
423  napply succ_plus.
424nqed.
425
426nlemma multiplication_zero_right_neutral:
427  ∀m: Nat.
428    m * Z = Z.
429  #m.
430  nelim m.
431  nnormalize.
432  @.
433  #N H.
434  nnormalize.
435  nrewrite > H.
436  @.
437nqed.
438
439nlemma multiplication_succ:
440  ∀m, n: Nat.
441    m * S(n) = m + (m * n).
442  #m n.
443  nelim m.
444  nnormalize.
445  @.
446  #N H.
447  nnormalize.
448  nrewrite > H.
449  nrewrite < (plus_associative n N ?).
450  nrewrite > (plus_symmetrical n N).
451  nrewrite > (plus_associative N n ?).
452  @.
453nqed.
454
455nlemma multiplication_symmetrical:
456  ∀m, n: Nat.
457    m * n = n * m.
458  #m n.
459  nelim m.
460  nnormalize.
461  nelim n.
462  nnormalize.
463  @.
464  #N H.
465  nnormalize.
466  nrewrite < H.
467  @.
468  #N H.
469  nnormalize.
470  nrewrite > H.
471  nrewrite > (multiplication_succ ? ?).
472  @.
473nqed.
474
475nlemma multiplication_succ_zero_left_neutral:
476  ∀m: Nat.
477    (S Z) * m = m.
478  #m.
479  nelim m.
480  nnormalize.
481  @.
482  #N H.
483  nnormalize.
484  nrewrite > (succ_plus ? ?).
485  nrewrite < (succ_plus_succ_zero ?).
486  @.
487nqed.
488
489nlemma multiplication_succ_zero_right_neutral:
490  ∀m: Nat.
491    m * (S Z) = m.
492  #m.
493  nelim m.
494  nnormalize.
495  @.
496  #N H.
497  nnormalize.
498  nrewrite > H.
499  @.
500nqed.
501
502nlemma multiplication_distributes_right_plus:
503  ∀m, n, o: Nat.
504    (m + n) * o = m * o + n * o.
505  #m n o.
506  nelim m.
507  nnormalize.
508  @.
509  #N H.
510  nnormalize.
511  nrewrite > H.
512  nrewrite < (plus_associative ? ? ?).
513  @.
514nqed.
515
516nlemma multiplication_distributes_left_plus:
517  ∀m, n, o: Nat.
518    o * (m + n) = o * m + o * n.
519  #m n o.
520  nelim o.
521  //.
522  #N H.
523  nnormalize.
524  nrewrite > H.
525  nrewrite < (plus_associative ? n (N * n)).
526  nrewrite > (plus_symmetrical (m + N * m) n).
527  nrewrite < (plus_associative n m (N * m)).
528  nrewrite < (plus_symmetrical n m).
529  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
530  @.
531nqed.
532
533nlemma mutliplication_associative:
534  ∀m, n, o: Nat.
535    m * (n * o) = (m * n) * o.
536  #m n o.
537  nelim m.
538  nnormalize.
539  @.
540  #N H.
541  nnormalize.
542  nrewrite > H.
543  nrewrite > (multiplication_distributes_right_plus ? ? ?).
544  @.
545nqed.
546
547nlemma minus_minus:
548  ∀n: Nat.
549    n - n = Z.
550  #n.
551  nelim n.
552  nnormalize.
553  @.
554  #N H.
555  nnormalize.
556  nrewrite > H.
557  @.
558nqed.
559
560
561nlemma succ_injective:
562  ∀m, n: Nat.
563    S m = S n → m = n.
564  #m n H;
565  napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with
566           [refl ⇒ ? ]);
567  @;
568nqed.
569
570ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'.
571 //;
572nqed.
573
574ntheorem plus_minus_inverse_right:
575  ∀m, n: Nat.
576   n ≤ m → (m - n) + n = m.
577 #m; nelim m
578  [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1);
579    #K; ncases (K H3)
580  | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/;
581    #w; nrewrite < succ_plus; /4/. ##]
582nqed.
583
584(*
585
586nlemma plus_minus_associate:
587  ∀m, n, o: Nat.
588    (m + n) - o = m + (n - o).
589  #m n o.
590  nelim m.
591  nnormalize.
592  @.
593  #N H.
594
595
596nlemma plus_minus_inverses:
597  ∀m, n: Nat.
598    (m + n) - n = m.
599  #m n.
600  nelim m.
601  nnormalize.
602  napply minus_minus.
603  #N H.
604*)
605
606ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n.
607 #m; nelim m; //; #y H1 z; ncases z; nnormalize
608  [ #H; ndestruct | /3/ ]
609nqed.
610
611ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n).
612 #m; nelim m; nnormalize
613  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
614    [ #H; /2/ | /3/ ]
615nqed.
616
617ndefinition less_than_or_equal_b_elim:
618 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
619  P (less_than_or_equal_b m n).
620 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
621 nlapply (less_than_or_equal_b_complete m n);
622 ncases (less_than_or_equal_b m n); /3/.
623nqed.
624
625ndefinition greater_than_or_equal_b_elim:
626 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) →
627  P (greater_than_or_equal_b m n).
628 #m n; napply less_than_or_equal_b_elim;
629nqed.
630
631ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n.
632 #m; nelim m
633  [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ]
634##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K;
635    napply less_than_or_equal_monotone; napply H; napply K ]
636nqed.
637
638ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n).
639 #m; nelim m
640  [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct
641  | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/.
642nqed.
643
644ndefinition less_than_b_elim:
645 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) →
646  P (less_than_b m n).
647 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n);
648 ncases (less_than_b m n); /3/.
649nqed.
650
651ndefinition greater_than_b_elim:
652 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) →
653  P (greater_than_b m n).
654 #m n; napply less_than_b_elim.
655nqed.
656
657nlemma less_than_or_equal_plus:
658  ∀n,m: Nat.
659    n ≤ n + m.
660  #n m.
661  nelim n.
662  //.
663  #N H.
664  napply (less_than_or_equal_monotone).
665  /2/.
666nqed.
667
668(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
669(* Numbers.                                                                   *)
670(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
671
672ndefinition one ≝ S Z.
673ndefinition two ≝ (S(S(Z))).
674ndefinition three ≝ two + one.
675ndefinition four ≝ two + two.
676ndefinition five ≝ three + two.
677ndefinition six ≝ three + three.
678ndefinition seven ≝ three + four.
679ndefinition eight ≝ four + four.
680ndefinition nine ≝ five + four.
681ndefinition ten ≝ five + five.
682ndefinition eleven ≝ six + five.
683ndefinition twelve ≝ six + six.
684ndefinition thirteen ≝ seven + six.
685ndefinition fourteen ≝ seven + seven.
686ndefinition fifteen ≝ eight + seven.
687ndefinition sixteen ≝ eight + eight.
688ndefinition seventeen ≝ nine + eight.
689ndefinition eighteen ≝ nine + nine.
690ndefinition nineteen ≝ ten + nine.
691ndefinition twenty_four ≝ sixteen + eight.
692ndefinition thirty_two ≝ sixteen + sixteen.
693ndefinition one_hundred ≝ ten * ten.
694ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
695ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
696ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
697ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
698ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
699ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
700ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
701ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
702ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
703ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
704ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
705ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
706ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
707ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
708ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
709ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
710ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
711ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
712ndefinition two_hundred ≝ one_hundred + one_hundred.
713ndefinition two_hundred_and_two ≝ two_hundred + two.
714ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
715ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
716ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
717ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
718ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
719ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
720ndefinition two_hundred_and_fifty_six ≝
721  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.
Note: See TracBrowser for help on using the repository browser.