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