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