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/plus.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 lemma sigma_p_gi: \forall g: nat \to Z.
 224 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 225 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 226 intros 2.
 227 elim n
 228   [apply False_ind.
 229    apply (not_le_Sn_O i).
 230    assumption
 231   |apply (bool_elim ? (p n1));intro
 232     [elim (le_to_or_lt_eq i n1)
 233       [rewrite > true_to_sigma_p_Sn
 234         [rewrite > true_to_sigma_p_Sn
 235           [rewrite < assoc_Zplus.
 236            rewrite < sym_Zplus in \vdash (? ? ? (? % ?)).
 237            rewrite > assoc_Zplus.
 238            apply eq_f2
 239             [reflexivity
 240             |apply H[assumption|assumption]
 241             ]
 242           |rewrite > H3.simplify.
 243            change with (notb (eqb n1 i) = notb false).
 244            apply eq_f.
 245            apply not_eq_to_eqb_false.
 246            unfold Not.intro.
 247            apply (lt_to_not_eq ? ? H4).
 248            apply sym_eq.assumption
 249           ]
 250         |assumption
 251         ]
 252       |rewrite > true_to_sigma_p_Sn
 253         [rewrite > H4.
 254          apply eq_f2
 255           [reflexivity
 256           |rewrite > false_to_sigma_p_Sn
 257             [apply eq_sigma_p
 258               [intros.
 259                elim (p x)
 260                 [simplify.
 261                  change with (notb false = notb (eqb x n1)).
 262                  apply eq_f.
 263                  apply sym_eq.
 264                  apply not_eq_to_eqb_false.
 265                  apply (lt_to_not_eq ? ? H5)
 266                 |reflexivity
 267                 ]
 268               |intros.reflexivity
 269               ]
 270             |rewrite > H3.
 271              rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
 272              reflexivity
 273             ]
 274           ]
 275         |assumption
 276         ]
 277       |apply le_S_S_to_le.assumption
 278       ]
 279     |rewrite > false_to_sigma_p_Sn
 280       [elim (le_to_or_lt_eq i n1)
 281         [rewrite > false_to_sigma_p_Sn
 282           [apply H[assumption|assumption]
 283           |rewrite > H3.reflexivity
 284           ]
 285         |apply False_ind.
 286          apply not_eq_true_false.
 287          rewrite < H2.
 288          rewrite > H4.
 289          assumption
 290         |apply le_S_S_to_le.assumption
 291         ]
 292       |assumption
 293       ]
 294     ]
 295   ]
 296 qed.
 297
 298 theorem eq_sigma_p_gh:
 299 \forall g: nat \to Z.
 300 \forall h,h1: nat \to nat.\forall n,n1.
 301 \forall p1,p2:nat \to bool.
 302 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 303 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 304 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 305 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 306 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 307 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 308 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
 309 intros 4.
 310 elim n
 311   [generalize in match H5.
 312    elim n1
 313     [reflexivity
 314     |apply (bool_elim ? (p2 n2));intro
 315       [apply False_ind.
 316        apply (not_le_Sn_O (h1 n2)).
 317        apply H7
 318         [apply le_n|assumption]
 319       |rewrite > false_to_sigma_p_Sn
 320         [apply H6.
 321          intros.
 322             apply H7[apply le_S.apply H9|assumption]
 323         |assumption
 324         ]
 325       ]
 326     ]
 327   |apply (bool_elim ? (p1 n1));intro
 328     [rewrite > true_to_sigma_p_Sn
 329       [rewrite > (sigma_p_gi g n2 (h n1))
 330         [apply eq_f2
 331           [reflexivity
 332           |apply H
 333             [intros.
 334              rewrite > H1
 335               [simplify.
 336                change with ((\not eqb (h i) (h n1))= \not false).
 337                apply eq_f.
 338                apply not_eq_to_eqb_false.
 339                unfold Not.intro.
 340                apply (lt_to_not_eq ? ? H8).
 341                rewrite < H2
 342                 [rewrite < (H2 n1)
 343                   [apply eq_f.assumption|apply le_n|assumption]
 344                 |apply le_S.assumption
 345                 |assumption
 346                 ]
 347               |apply le_S.assumption
 348               |assumption
 349               ]
 350             |intros.
 351              apply H2[apply le_S.assumption|assumption]
 352             |intros.
 353              apply H3[apply le_S.assumption|assumption]
 354             |intros.
 355              apply H4
 356               [assumption
 357               |generalize in match H9.
 358                elim (p2 j)
 359                 [reflexivity|assumption]
 360               ]
 361             |intros.
 362              apply H5
 363               [assumption
 364               |generalize in match H9.
 365                elim (p2 j)
 366                 [reflexivity|assumption]
 367               ]
 368             |intros.
 369              elim (le_to_or_lt_eq (h1 j) n1)
 370               [assumption
 371               |generalize in match H9.
 372                elim (p2 j)
 373                 [simplify in H11.
 374                  absurd (j = (h n1))
 375                   [rewrite < H10.
 376                    rewrite > H5
 377                     [reflexivity|assumption|auto]
 378                   |apply eqb_false_to_not_eq.
 379                    generalize in match H11.
 380                    elim (eqb j (h n1))
 381                     [apply sym_eq.assumption|reflexivity]
 382                   ]
 383                 |simplify in H11.
 384                  apply False_ind.
 385                  apply not_eq_true_false.
 386                  apply sym_eq.assumption
 387                 ]
 388               |apply le_S_S_to_le.
 389                apply H6
 390                 [assumption
 391                 |generalize in match H9.
 392                  elim (p2 j)
 393                   [reflexivity|assumption]
 394                 ]
 395               ]
 396             ]
 397           ]
 398         |apply H3[apply le_n|assumption]
 399         |apply H1[apply le_n|assumption]
 400         ]
 401       |assumption
 402       ]
 403     |rewrite > false_to_sigma_p_Sn
 404      [apply H
 405        [intros.apply H1[apply le_S.assumption|assumption]
 406        |intros.apply H2[apply le_S.assumption|assumption]
 407        |intros.apply H3[apply le_S.assumption|assumption]
 408        |intros.apply H4[assumption|assumption]
 409        |intros.apply H5[assumption|assumption]
 410        |intros.
 411         elim (le_to_or_lt_eq (h1 j) n1)
 412           [assumption
 413           |absurd (j = (h n1))
 414             [rewrite < H10.
 415              rewrite > H5
 416                [reflexivity|assumption|assumption]
 417             |unfold Not.intro.
 418              apply not_eq_true_false.
 419              rewrite < H7.
 420              rewrite < H10.
 421              rewrite > H4
 422               [reflexivity|assumption|assumption]
 423             ]
 424           |apply le_S_S_to_le.
 425            apply H6[assumption|assumption]
 426           ]
 427         ]
 428       |assumption
 429       ]
 430     ]
 431   ]
 432 qed.
 433
 434 definition p_ord_times \def
 435 \lambda p,m,x.
 436   match p_ord x p with
 437   [pair q r \Rightarrow r*m+q].
 438
 439 theorem  eq_p_ord_times: \forall p,m,x.
 440 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
 441 intros.unfold p_ord_times. unfold ord_rem.
 442 unfold ord.
 443 elim (p_ord x p).
 444 reflexivity.
 445 qed.
 446
 447 theorem div_p_ord_times:
 448 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
 449 intros.rewrite > eq_p_ord_times.
 450 apply div_plus_times.
 451 assumption.
 452 qed.
 453
 454 theorem mod_p_ord_times:
 455 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
 456 intros.rewrite > eq_p_ord_times.
 457 apply mod_plus_times.
 458 assumption.
 459 qed.
 460
 461 theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
 462 apply nat_elim2;intros
 463   [left.reflexivity
 464   |right.reflexivity
 465   |apply False_ind.
 466    simplify in H1.
 467    apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
 468   ]
 469 qed.
 470
 471 theorem prime_to_lt_O: \forall p. prime p \to O < p.
 472 intros.elim H.apply lt_to_le.assumption.
 473 qed.
 474
 475 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
 476 p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
 477 intros.
 478 cut (m = ord (n*(exp p m)) p)
 479   [apply le_S_S.
 480    rewrite > Hcut.
 481    apply divides_to_le_ord
 482     [elim (le_to_or_lt_eq ? ? (le_O_n j))
 483       [assumption
 484       |apply False_ind.
 485        apply (lt_to_not_eq ? ? H).
 486        elim H3.
 487        rewrite < H4 in H5.simplify in H5.
 488        elim (times_O_to_O ? ? H5)
 489         [apply sym_eq.assumption
 490         |apply False_ind.
 491          apply (not_le_Sn_n O).
 492          rewrite < H6 in \vdash (? ? %).
 493          apply lt_O_exp.
 494          elim H1.apply lt_to_le.assumption
 495         ]
 496       ]
 497     |rewrite > (times_n_O O).
 498      apply lt_times
 499       [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
 500     |assumption
 501     |assumption
 502     ]
 503   |unfold ord.
 504    rewrite > (p_ord_exp1 p ? m n)
 505     [reflexivity
 506     |apply (prime_to_lt_O ? H1)
 507     |assumption
 508     |apply sym_times
 509     ]
 510   ]
 511 qed.
 512
 513 theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
 514 p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
 515 intros.
 516 cut (O < j)
 517   [cut (n = ord_rem (n*(exp p m)) p)
 518     [rewrite > Hcut1.
 519      apply divides_to_divides_ord_rem
 520       [assumption
 521       |rewrite > (times_n_O O).
 522        apply lt_times
 523         [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
 524       |assumption
 525       |assumption
 526       ]
 527     |unfold ord_rem.
 528      rewrite > (p_ord_exp1 p ? m n)
 529       [reflexivity
 530       |apply (prime_to_lt_O ? H1)
 531       |assumption
 532       |apply sym_times
 533       ]
 534     ]
 535   |elim (le_to_or_lt_eq ? ? (le_O_n j))
 536     [assumption
 537     |apply False_ind.
 538      apply (lt_to_not_eq ? ? H).
 539      elim H3.
 540      rewrite < H4 in H5.simplify in H5.
 541      elim (times_O_to_O ? ? H5)
 542       [apply sym_eq.assumption
 543       |apply False_ind.
 544        apply (not_le_Sn_n O).
 545        rewrite < H6 in \vdash (? ? %).
 546        apply lt_O_exp.
 547        elim H1.apply lt_to_le.assumption
 548       ]
 549     ]
 550   ]
 551 qed.
 552
 553 theorem sigma_p_divides_b:
 554 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 555 \forall g: nat \to Z.
 556 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 557 sigma_p (S n) (\lambda x.divides_b x n)
 558   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 559 intros.
 560 cut (O < p)
 561   [rewrite < sigma_p2.
 562    apply (trans_eq ? ?
 563     (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
 564        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
 565     [apply sym_eq.
 566      apply (eq_sigma_p_gh g ? (p_ord_times p (S m)))
 567       [intros.
 568        lapply (divides_b_true_to_lt_O ? ? H H4).
 569        apply divides_to_divides_b_true
 570         [rewrite > (times_n_O O).
 571          apply lt_times
 572           [assumption
 573           |apply lt_O_exp.assumption
 574           ]
 575         |apply divides_times
 576           [apply divides_b_true_to_divides.assumption
 577           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
 578            rewrite < exp_plus_times.
 579            apply eq_f.
 580            rewrite > sym_plus.
 581            apply plus_minus_m_m.
 582            auto
 583           ]
 584         ]
 585       |intros.
 586        lapply (divides_b_true_to_lt_O ? ? H H4).
 587        unfold p_ord_times.
 588        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
 589         [change with ((i/S m)*S m+i \mod S m=i).
 590          apply sym_eq.
 591          apply div_mod.
 592          apply lt_O_S
 593         |assumption
 594         |unfold Not.intro.
 595          apply H2.
 596          apply (trans_divides ? (i/ S m))
 597           [assumption|
 598            apply divides_b_true_to_divides;assumption]
 599         |apply sym_times.
 600         ]
 601       |intros.
 602        apply le_S_S.
 603        apply le_times
 604         [apply le_S_S_to_le.
 605          change with ((i/S m) < S n).
 606          apply (lt_times_to_lt_l m).
 607          apply (le_to_lt_to_lt ? i)
 608           [auto|assumption]
 609         |apply le_exp
 610           [assumption
 611           |apply le_S_S_to_le.
 612            apply lt_mod_m_m.
 613            apply lt_O_S
 614           ]
 615         ]
 616       |intros.
 617        cut (ord j p < S m)
 618         [rewrite > div_p_ord_times
 619           [apply divides_to_divides_b_true
 620             [apply lt_O_ord_rem
 621               [elim H1.assumption
 622               |apply (divides_b_true_to_lt_O ? ? ? H4).
 623                 rewrite > (times_n_O O).
 624                 apply lt_times
 625                 [assumption|apply lt_O_exp.assumption]
 626               ]
 627             |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
 628              apply divides_b_true_to_divides.
 629              assumption
 630             ]
 631             |assumption
 632           ]
 633         |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
 634          apply (divides_b_true_to_divides ? ? H4).
 635          apply (divides_b_true_to_lt_O ? ? H4)
 636         ]
 637       |intros.
 638        cut (ord j p < S m)
 639         [rewrite > div_p_ord_times
 640           [rewrite > mod_p_ord_times
 641             [rewrite > sym_times.
 642              apply sym_eq.
 643              apply exp_ord
 644               [elim H1.assumption
 645               |apply (divides_b_true_to_lt_O ? ? ? H4).
 646                rewrite > (times_n_O O).
 647                apply lt_times
 648                 [assumption|apply lt_O_exp.assumption]
 649               ]
 650             |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
 651              apply (divides_b_true_to_divides ? ? H4).
 652              apply (divides_b_true_to_lt_O ? ? H4)
 653             ]
 654           |assumption
 655           ]
 656         |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
 657          apply (divides_b_true_to_divides ? ? H4).
 658          apply (divides_b_true_to_lt_O ? ? H4).
 659         ]
 660       |intros.
 661        rewrite > eq_p_ord_times.
 662        rewrite > sym_plus.
 663        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
 664         [apply lt_plus_l.
 665          apply le_S_S.
 666          cut (m = ord (n*(p \sup m)) p)
 667           [rewrite > Hcut1.
 668            apply divides_to_le_ord
 669             [apply (divides_b_true_to_lt_O ? ? ? H4).
 670              rewrite > (times_n_O O).
 671              apply lt_times
 672               [assumption|apply lt_O_exp.assumption]
 673             |rewrite > (times_n_O O).
 674              apply lt_times
 675               [assumption|apply lt_O_exp.assumption]
 676             |assumption
 677             |apply divides_b_true_to_divides.
 678              assumption
 679             ]
 680           |unfold ord.
 681            rewrite > sym_times.
 682            rewrite > (p_ord_exp1 p ? m n)
 683             [reflexivity
 684             |assumption
 685             |assumption
 686             |reflexivity
 687             ]
 688           ]
 689         |change with (S (ord_rem j p)*S m \le S n*S m).
 690          apply le_times_l.
 691          apply le_S_S.
 692          apply divides_to_le
 693           [assumption
 694           |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
 695            apply divides_b_true_to_divides.
 696            assumption
 697           ]
 698         ]
 699       ]
 700     |apply eq_sigma_p
 701       [intros.
 702        elim (divides_b (x/S m) n);reflexivity
 703       |intros.reflexivity
 704       ]
 705     ]
 706   |elim H1.apply lt_to_le.assumption
 707   ]
 708 qed.
 709