]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/sigma_p.ma
- transcript: we have now two styles of mma's from grafite:
[helm.git] / helm / software / matita / library / Z / sigma_p.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Z/times.ma".
16 include "nat/primes.ma".
17 include "nat/ord.ma".
18 include "nat/generic_iter_p.ma".
19
20 (* sigma_p in Z is a specialization of iter_p_gen *)
21 definition sigma_p: nat \to (nat \to bool) \to (nat \to Z) \to Z \def
22 \lambda n, p, g. (iter_p_gen n p Z g OZ Zplus).
23
24 theorem symmetricZPlus: symmetric Z Zplus.
25 change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)).
26 intros.
27 rewrite > sym_Zplus.
28 reflexivity.
29 qed.
30    
31 theorem true_to_sigma_p_Sn: 
32 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
33 p n = true \to sigma_p (S n) p g = 
34 (g n)+(sigma_p n p g).
35 intros.
36 unfold sigma_p.
37 apply true_to_iter_p_gen_Sn.
38 assumption.
39 qed.
40    
41 theorem false_to_sigma_p_Sn: 
42 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
43 p n = false \to sigma_p (S n) p g = sigma_p n p g.
44 intros.
45 unfold sigma_p.
46 apply false_to_iter_p_gen_Sn.
47 assumption.
48 qed.
49
50 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
51 \forall g1,g2: nat \to Z.\forall n.
52 (\forall x.  x < n \to p1 x = p2 x) \to
53 (\forall x.  x < n \to g1 x = g2 x) \to
54 sigma_p n p1 g1 = sigma_p n p2 g2.
55 intros.
56 unfold sigma_p.
57 apply eq_iter_p_gen;
58   assumption.
59 qed.
60
61 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
62 \forall g1,g2: nat \to Z.\forall n.
63 (\forall x.  x < n \to p1 x = p2 x) \to
64 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
65 sigma_p n p1 g1 = sigma_p n p2 g2.
66 intros.
67 unfold sigma_p.
68 apply eq_iter_p_gen1;
69   assumption.
70 qed.
71
72 theorem sigma_p_false: 
73 \forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O.
74 intros.
75 unfold sigma_p.
76 apply iter_p_gen_false.
77 qed.
78
79 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
80 \forall g: nat \to Z.
81 sigma_p (k+n) p g 
82 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
83 intros.
84 unfold sigma_p.
85 apply (iter_p_gen_plusA Z n k p g OZ Zplus)
86 [ apply symmetricZPlus.
87 | intros.
88   apply Zplus_z_OZ.
89 | apply associative_Zplus
90 ]
91 qed.
92
93 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
94 \forall p:nat \to bool.
95 \forall g: nat \to Z. (\forall i:nat. n \le i \to i < m \to
96 p i = false) \to sigma_p m p g = sigma_p n p g.
97 intros.
98 unfold sigma_p.
99 apply (false_to_eq_iter_p_gen);
100   assumption.
101 qed.
102
103 theorem sigma_p2 : 
104 \forall n,m:nat.
105 \forall p1,p2:nat \to bool.
106 \forall g: nat \to nat \to Z.
107 sigma_p (n*m) 
108   (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
109   (\lambda x.g (div x m) (mod x m)) =
110 sigma_p n p1 
111   (\lambda x.sigma_p m p2 (g x)).
112 intros.
113 unfold sigma_p.
114 apply (iter_p_gen2 n m p1 p2 Z g OZ Zplus)
115 [ apply symmetricZPlus
116 | apply associative_Zplus
117 | intros.
118   apply Zplus_z_OZ
119 ]
120 qed.
121
122 (* a stronger, dependent version, required e.g. for dirichlet product *)
123
124 theorem sigma_p2' : 
125 \forall n,m:nat.
126 \forall p1:nat \to bool.
127 \forall p2:nat \to nat \to bool.
128 \forall g: nat \to nat \to Z.
129 sigma_p (n*m) 
130   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) 
131   (\lambda x.g (div x m) (mod x m)) =
132 sigma_p n p1 
133   (\lambda x.sigma_p m (p2 x) (g x)).
134 intros.
135 unfold sigma_p.
136 apply (iter_p_gen2' n m p1 p2 Z g OZ Zplus)
137 [ apply symmetricZPlus
138 | apply associative_Zplus
139 | intros.
140   apply Zplus_z_OZ
141 ]
142 qed.
143
144 lemma sigma_p_gi: \forall g: nat \to Z.
145 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
146 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
147 intros.
148 unfold sigma_p.
149 apply (iter_p_gen_gi)
150 [ apply symmetricZPlus
151 | apply associative_Zplus
152 | intros.
153   apply Zplus_z_OZ
154 | assumption
155 | assumption
156 ]
157 qed.
158
159 theorem eq_sigma_p_gh: 
160 \forall g: nat \to Z.
161 \forall h,h1: nat \to nat.\forall n,n1.
162 \forall p1,p2:nat \to bool.
163 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
164 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
165 (\forall i. i < n \to p1 i = true \to h i < n1) \to 
166 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
167 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
168 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
169 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
170 intros.
171 unfold sigma_p.
172 apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2)
173 [ apply symmetricZPlus
174 | apply associative_Zplus
175 | intros.
176   apply Zplus_z_OZ
177 | assumption
178 | assumption
179 | assumption
180 | assumption
181 | assumption
182 | assumption
183 ]
184 qed.
185
186
187 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
188 p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
189 intros.
190 cut (m = ord (n*(exp p m)) p)
191   [apply le_S_S.
192    rewrite > Hcut.
193    apply divides_to_le_ord
194     [elim (le_to_or_lt_eq ? ? (le_O_n j))
195       [assumption
196       |apply False_ind.
197        apply (lt_to_not_eq ? ? H).
198        elim H3.
199        rewrite < H4 in H5.simplify in H5.
200        elim (times_O_to_O ? ? H5)
201         [apply sym_eq.assumption
202         |apply False_ind.
203          apply (not_le_Sn_n O).
204          rewrite < H6 in \vdash (? ? %).
205          apply lt_O_exp.
206          elim H1.apply lt_to_le.assumption
207         ]
208       ]
209     |rewrite > (times_n_O O).
210      apply lt_times
211       [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
212     |assumption
213     |assumption
214     ]
215   |unfold ord.
216    rewrite > (p_ord_exp1 p ? m n)
217     [reflexivity
218     |apply (prime_to_lt_O ? H1)
219     |assumption
220     |apply sym_times
221     ]
222   ]
223 qed.
224
225 theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
226 p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
227 intros.
228 cut (O < j)
229   [cut (n = ord_rem (n*(exp p m)) p)
230     [rewrite > Hcut1.
231      apply divides_to_divides_ord_rem
232       [assumption   
233       |rewrite > (times_n_O O).
234        apply lt_times
235         [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
236       |assumption
237       |assumption
238       ]
239     |unfold ord_rem.
240      rewrite > (p_ord_exp1 p ? m n)
241       [reflexivity
242       |apply (prime_to_lt_O ? H1)
243       |assumption
244       |apply sym_times
245       ]
246     ]
247   |elim (le_to_or_lt_eq ? ? (le_O_n j))
248     [assumption
249     |apply False_ind.
250      apply (lt_to_not_eq ? ? H).
251      elim H3.
252      rewrite < H4 in H5.simplify in H5.
253      elim (times_O_to_O ? ? H5)
254       [apply sym_eq.assumption
255       |apply False_ind.
256        apply (not_le_Sn_n O).
257        rewrite < H6 in \vdash (? ? %).
258        apply lt_O_exp.
259        elim H1.apply lt_to_le.assumption
260       ]
261     ]
262   ] 
263 qed.
264
265
266 theorem sigma_p_divides_b: 
267 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
268 \forall g: nat \to Z.
269 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
270 sigma_p (S n) (\lambda x.divides_b x n)
271   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
272 intros.
273 unfold sigma_p.
274 apply (iter_p_gen_divides Z OZ Zplus n m p ? ? ? g)
275 [ assumption
276 | assumption
277 | assumption
278 | apply symmetricZPlus
279 | apply associative_Zplus
280 | intros.
281   apply Zplus_z_OZ
282 ]
283 qed.
284
285     
286 (* sigma_p and Ztimes *)
287 lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
288 z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
289 intros.
290 apply (distributive_times_plus_iter_p_gen Z Zplus OZ Ztimes n z p f)
291 [ apply symmetricZPlus
292 | apply associative_Zplus
293 | intros.
294   apply Zplus_z_OZ
295 | apply symmetric_Ztimes
296 | apply distributive_Ztimes_Zplus
297 | intros.
298   rewrite > (Ztimes_z_OZ a).
299   reflexivity
300 ]
301 qed.
302
303 lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f.
304 (sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z).
305 intros.
306 rewrite < sym_Ztimes.
307 rewrite > Ztimes_sigma_pl.
308 apply eq_sigma_p
309   [intros.reflexivity
310   |intros.apply sym_Ztimes
311   ]
312 qed.
313
314
315 theorem sigma_p_knm: 
316 \forall g: nat \to Z.
317 \forall h2:nat \to nat \to nat.
318 \forall h11,h12:nat \to nat. 
319 \forall k,n,m.
320 \forall p1,p21:nat \to bool.
321 \forall p22:nat \to nat \to bool.
322 (\forall x. x < k \to p1 x = true \to 
323 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
324 \land h2 (h11 x) (h12 x) = x 
325 \land (h11 x) < n \land (h12 x) < m) \to
326 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
327 p1 (h2 i j) = true \land 
328 h11 (h2 i j) = i \land h12 (h2 i j) = j
329 \land h2 i j < k) \to
330 sigma_p k p1 g=
331 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
332 intros.
333 unfold sigma_p.
334 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
335 apply iter_p_gen_knm
336   [ apply symmetricZPlus
337   |apply associative_Zplus
338   | intro.
339     apply (Zplus_z_OZ a)
340   | exact h11
341   | exact h12
342   | assumption
343   | assumption
344   ]
345 qed.
346
347
348 theorem sigma_p2_eq: 
349 \forall g: nat \to nat \to Z.
350 \forall h11,h12,h21,h22: nat \to nat \to nat. 
351 \forall n1,m1,n2,m2.
352 \forall p11,p21:nat \to bool.
353 \forall p12,p22:nat \to nat \to bool.
354 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
355 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
356 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
357 \land h11 i j < n1 \land h12 i j < m1) \to
358 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
359 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
360 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
361 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
362 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
363 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
364 intros.
365 unfold sigma_p.
366 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
367 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
368
369 apply(iter_p_gen_2_eq Z OZ Zplus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
370 [ apply symmetricZPlus
371 | apply associative_Zplus
372 | intro.
373   apply (Zplus_z_OZ a)
374 | assumption
375 | assumption
376 ]
377 qed.
378
379
380
381
382 (*
383
384
385
386
387
388 rewrite < sigma_p2'.
389 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
390 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
391 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
392
393 apply (trans_eq ? ? 
394 (sigma_p n2 p21 (\lambda x:nat. sigma_p m2 (p22 x)
395  (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1)) ) ) ))
396 [
397   apply (sigma_p_knm (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
398   [ elim (and_true ? ? H3).
399     cut(O \lt m1)
400     [ cut(x/m1 < n1)
401       [ cut((x \mod m1) < m1)
402         [ elim (H1 ? ? Hcut1 Hcut2 H4 H5).
403           elim H6.clear H6.
404           elim H8.clear H8.
405           elim H6.clear H6.
406           elim H8.clear H8.
407           split
408           [ split
409             [ split
410               [ split
411                 [ assumption
412                 | assumption
413                 ]
414               | rewrite > H11.
415                 rewrite > H10.
416                 apply sym_eq.
417                 apply div_mod.
418                 assumption
419               ]
420             | assumption
421             ]
422           | assumption
423           ]
424         | apply lt_mod_m_m.
425           assumption
426         ]
427       | apply (lt_times_n_to_lt m1)
428         [ assumption
429         | apply (le_to_lt_to_lt ? x)
430           [ apply (eq_plus_to_le ? ? (x \mod m1)).
431             apply div_mod.
432             assumption
433           | assumption
434         ]
435       ]  
436     ]
437     | apply not_le_to_lt.unfold.intro.
438       generalize in match H2.
439       apply (le_n_O_elim ? H6).
440       rewrite < times_n_O.
441       apply le_to_not_lt.
442       apply le_O_n.              
443     ]
444   | elim (H ? ? H2 H3 H4 H5).
445     elim H6.clear H6.
446     elim H8.clear H8.
447     elim H6.clear H6.
448     elim H8.clear H8.
449     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
450     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
451       [ split
452         [ split
453           [ split
454             [ apply true_to_true_to_andb_true
455               [ rewrite > Hcut.
456                 assumption
457               | rewrite > Hcut1.
458                 rewrite > Hcut.
459                 assumption
460               ] 
461             | rewrite > Hcut1.
462               rewrite > Hcut.
463               assumption
464             ]
465           | rewrite > Hcut1.
466             rewrite > Hcut.
467             assumption            
468           ]
469         | cut(O \lt m1)
470           [ cut(O \lt n1)      
471             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
472               [ apply (lt_plus_r).
473                 assumption
474               | rewrite > sym_plus.
475                 rewrite > (sym_times (h11 i j) m1).
476                 rewrite > times_n_Sm.
477                 rewrite > sym_times.
478                 apply (le_times_l).
479                 assumption  
480               ]
481             | apply not_le_to_lt.unfold.intro.
482               generalize in match H9.
483               apply (le_n_O_elim ? H8).       
484               apply le_to_not_lt.
485               apply le_O_n
486             ]
487           | apply not_le_to_lt.unfold.intro.
488             generalize in match H7.
489             apply (le_n_O_elim ? H8).       
490             apply le_to_not_lt.
491             apply le_O_n
492           ]  
493         ]
494       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
495         reflexivity.
496         assumption
497       ]     
498     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
499       reflexivity.
500       assumption
501     ]
502   ]
503 | apply (eq_sigma_p1)
504   [ intros. reflexivity
505   | intros.
506     apply (eq_sigma_p1)
507     [ intros. reflexivity
508     | intros.
509       rewrite > (div_plus_times)
510       [ rewrite > (mod_plus_times)
511         [ reflexivity
512         | elim (H x x1 H2 H4 H3 H5).
513           assumption
514         ]
515       | elim (H x x1 H2 H4 H3 H5).       
516         assumption
517       ]
518     ]
519   ]
520 ]
521 qed.
522
523 rewrite < sigma_p2' in \vdash (? ? ? %).
524 apply sym_eq.
525 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
526 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
527 apply (trans_eq ? ? 
528   (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2))
529   (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1))))
530   [clear h.clear h1.
531    apply eq_sigma_p1
532     [intros.reflexivity
533     |intros.
534      cut (O < m2)
535       [cut (x/m2 < n2)
536         [cut (x \mod m2 < m2)
537           [elim (and_true ? ? H3).
538            elim (H ? ? Hcut1 Hcut2 H4 H5).
539            elim H6.clear H6.
540            elim H8.clear H8.
541            elim H6.clear H6.
542            elim H8.clear H8.
543            apply eq_f2
544             [apply sym_eq.
545              apply div_plus_times.
546              assumption
547             | 
548               apply sym_eq.
549               apply mod_plus_times.
550               assumption
551             ]
552           |apply lt_mod_m_m.
553            assumption
554           ]
555         |apply (lt_times_n_to_lt m2)
556           [assumption
557           |apply (le_to_lt_to_lt ? x)
558             [apply (eq_plus_to_le ? ? (x \mod m2)).
559              apply div_mod.
560              assumption
561             |assumption
562             ]
563           ]
564         ]
565       |apply not_le_to_lt.unfold.intro.
566        generalize in match H2.
567        apply (le_n_O_elim ? H4).
568        rewrite < times_n_O.
569        apply le_to_not_lt.
570        apply le_O_n  
571       ]      
572     ]
573   |apply (eq_sigma_p_gh ? h h1);intros
574     [cut (O < m2)
575       [cut (i/m2 < n2)
576         [cut (i \mod m2 < m2)
577           [elim (and_true ? ? H3).
578            elim (H ? ? Hcut1 Hcut2 H4 H5).
579            elim H6.clear H6.
580            elim H8.clear H8.
581            elim H6.clear H6.
582            elim H8.clear H8.
583            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
584                  h11 (i/m2) (i\mod m2))
585             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
586                   h12 (i/m2) (i\mod m2))
587               [rewrite > Hcut3.
588                rewrite > Hcut4.
589                rewrite > H6.
590                rewrite > H12.
591                reflexivity
592               |apply mod_plus_times. 
593                assumption
594               ]
595             |apply div_plus_times.
596              assumption
597             ]
598           |apply lt_mod_m_m.
599            assumption
600           ]
601         |apply (lt_times_n_to_lt m2)
602           [assumption
603           |apply (le_to_lt_to_lt ? i)
604             [apply (eq_plus_to_le ? ? (i \mod m2)).
605              apply div_mod.
606              assumption
607             |assumption
608             ]
609           ]
610         ]
611       |apply not_le_to_lt.unfold.intro.
612        generalize in match H2.
613        apply (le_n_O_elim ? H4).
614        rewrite < times_n_O.
615        apply le_to_not_lt.
616        apply le_O_n  
617       ]      
618     |cut (O < m2)
619       [cut (i/m2 < n2)
620         [cut (i \mod m2 < m2)
621           [elim (and_true ? ? H3).
622            elim (H ? ? Hcut1 Hcut2 H4 H5).
623            elim H6.clear H6.
624            elim H8.clear H8.
625            elim H6.clear H6.
626            elim H8.clear H8.
627            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
628                  h11 (i/m2) (i\mod m2))
629             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
630                   h12 (i/m2) (i\mod m2))
631               [rewrite > Hcut3.
632                rewrite > Hcut4.
633                rewrite > H10.
634                rewrite > H11.
635                apply sym_eq.
636                apply div_mod.
637                assumption
638               |apply mod_plus_times. 
639                assumption
640               ]
641             |apply div_plus_times.
642              assumption
643             ]
644           |apply lt_mod_m_m.
645            assumption
646           ]
647         |apply (lt_times_n_to_lt m2)
648           [assumption
649           |apply (le_to_lt_to_lt ? i)
650             [apply (eq_plus_to_le ? ? (i \mod m2)).
651              apply div_mod.
652              assumption
653             |assumption
654             ]
655           ]
656         ]
657       |apply not_le_to_lt.unfold.intro.
658        generalize in match H2.
659        apply (le_n_O_elim ? H4).
660        rewrite < times_n_O.
661        apply le_to_not_lt.
662        apply le_O_n  
663       ]      
664     |cut (O < m2)
665       [cut (i/m2 < n2)
666         [cut (i \mod m2 < m2)
667           [elim (and_true ? ? H3).
668            elim (H ? ? Hcut1 Hcut2 H4 H5).
669            elim H6.clear H6.
670            elim H8.clear H8.
671            elim H6.clear H6.
672            elim H8.clear H8.
673            apply lt_times_plus_times
674             [assumption|assumption]
675           |apply lt_mod_m_m.
676            assumption
677           ]
678         |apply (lt_times_n_to_lt m2)
679           [assumption
680           |apply (le_to_lt_to_lt ? i)
681             [apply (eq_plus_to_le ? ? (i \mod m2)).
682              apply div_mod.
683              assumption
684             |assumption
685             ]
686           ]
687         ]
688       |apply not_le_to_lt.unfold.intro.
689        generalize in match H2.
690        apply (le_n_O_elim ? H4).
691        rewrite < times_n_O.
692        apply le_to_not_lt.
693        apply le_O_n  
694       ]
695     |cut (O < m1)
696       [cut (j/m1 < n1)
697         [cut (j \mod m1 < m1)
698           [elim (and_true ? ? H3).
699            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
700            elim H6.clear H6.
701            elim H8.clear H8.
702            elim H6.clear H6.
703            elim H8.clear H8.
704            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
705                  h21 (j/m1) (j\mod m1))
706             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
707                   h22 (j/m1) (j\mod m1))
708               [rewrite > Hcut3.
709                rewrite > Hcut4.
710                rewrite > H6.
711                rewrite > H12.
712                reflexivity
713               |apply mod_plus_times. 
714                assumption
715               ]
716             |apply div_plus_times.
717              assumption
718             ]
719           |apply lt_mod_m_m.
720            assumption
721           ] 
722         |apply (lt_times_n_to_lt m1)
723           [assumption
724           |apply (le_to_lt_to_lt ? j)
725             [apply (eq_plus_to_le ? ? (j \mod m1)).
726              apply div_mod.
727              assumption
728             |assumption
729             ]
730           ]
731         ]
732       |apply not_le_to_lt.unfold.intro.
733        generalize in match H2.
734        apply (le_n_O_elim ? H4).
735        rewrite < times_n_O.
736        apply le_to_not_lt.
737        apply le_O_n  
738       ] 
739     |cut (O < m1)
740       [cut (j/m1 < n1)
741         [cut (j \mod m1 < m1)
742           [elim (and_true ? ? H3).
743            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
744            elim H6.clear H6.
745            elim H8.clear H8.
746            elim H6.clear H6.
747            elim H8.clear H8.
748            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
749                  h21 (j/m1) (j\mod m1))
750             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
751                   h22 (j/m1) (j\mod m1))
752               [rewrite > Hcut3.
753                rewrite > Hcut4.               
754                rewrite > H10.
755                rewrite > H11.
756                apply sym_eq.
757                apply div_mod.
758                assumption
759               |apply mod_plus_times. 
760                assumption
761               ]
762             |apply div_plus_times.
763              assumption
764             ]
765           |apply lt_mod_m_m.
766            assumption
767           ] 
768         |apply (lt_times_n_to_lt m1)
769           [assumption
770           |apply (le_to_lt_to_lt ? j)
771             [apply (eq_plus_to_le ? ? (j \mod m1)).
772              apply div_mod.
773              assumption
774             |assumption
775             ]
776           ]
777         ]
778       |apply not_le_to_lt.unfold.intro.
779        generalize in match H2.
780        apply (le_n_O_elim ? H4).
781        rewrite < times_n_O.
782        apply le_to_not_lt.
783        apply le_O_n  
784       ] 
785     |cut (O < m1)
786       [cut (j/m1 < n1)
787         [cut (j \mod m1 < m1)
788           [elim (and_true ? ? H3).
789            elim (H1 ? ? Hcut1 Hcut2 H4 H5).
790            elim H6.clear H6.
791            elim H8.clear H8.
792            elim H6.clear H6.
793            elim H8.clear H8.
794            apply (lt_times_plus_times ? ? ? m2)
795             [assumption|assumption]
796           |apply lt_mod_m_m.
797            assumption
798           ] 
799         |apply (lt_times_n_to_lt m1)
800           [assumption
801           |apply (le_to_lt_to_lt ? j)
802             [apply (eq_plus_to_le ? ? (j \mod m1)).
803              apply div_mod.
804              assumption
805             |assumption
806             ]
807           ]
808         ]
809       |apply not_le_to_lt.unfold.intro.
810        generalize in match H2.
811        apply (le_n_O_elim ? H4).
812        rewrite < times_n_O.
813        apply le_to_not_lt.
814        apply le_O_n  
815       ]
816     ]
817   ]
818 qed.
819 *)
820
821