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