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