helm/software/matita/library/nat/ord.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 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "datatypes/constructors.ma".
  16 include "nat/exp.ma".
  17 include "nat/nth_prime.ma".
  18 include "nat/gcd.ma". (* for some properties of divides *)
  19 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
  20
  21 let rec p_ord_aux p n m \def
  22   match n \mod m with
  23   [ O \Rightarrow
  24     match p with
  25       [ O \Rightarrow pair nat nat O n
  26       | (S p) \Rightarrow
  27        match (p_ord_aux p (n / m) m) with
  28        [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
  29   | (S a) \Rightarrow pair nat nat O n].
  30
  31 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
  32 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
  33
  34 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
  35   match p_ord_aux p n m with
  36   [ (pair q r) \Rightarrow n = m \sup q *r ].
  37 intro.
  38 elim p.simplify.
  39 apply (nat_case (n \mod m)).
  40 simplify.apply plus_n_O.
  41 intros.
  42 simplify.apply plus_n_O.
  43 simplify.
  44 apply (nat_case1 (n1 \mod m)).intro.
  45 simplify.
  46 generalize in match (H (n1 / m) m).
  47 elim (p_ord_aux n (n1 / m) m).
  48 simplify.
  49 rewrite > assoc_times.
  50 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
  51 rewrite < H2.
  52 rewrite > sym_times.
  53 rewrite < div_mod.reflexivity.
  54 assumption.assumption.
  55 intros.simplify.apply plus_n_O.
  56 qed.
  57
  58 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
  59   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
  60 intros.
  61 change with
  62 match (pair nat nat q r) with
  63   [ (pair q r) \Rightarrow n = m \sup q * r ].
  64 rewrite > H1.
  65 apply p_ord_aux_to_Prop.
  66 assumption.
  67 qed.
  68
  69 (* questo va spostato in primes1.ma *)
  70 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
  71 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
  72 intros 5.
  73 elim i.
  74 simplify.
  75 rewrite < plus_n_O.
  76 apply (nat_case p).
  77 simplify.
  78 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
  79 intro.
  80 simplify.
  81 cut (O < n \mod m \lor O = n \mod m).
  82 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
  83 intros. simplify.reflexivity.
  84 apply False_ind.
  85 apply H1.apply sym_eq.assumption.
  86 apply le_to_or_lt_eq.apply le_O_n.
  87 generalize in match H3.
  88 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
  89 intros.
  90 simplify. fold simplify (m \sup (S n1)).
  91 cut (((m \sup (S n1)*n) \mod m) = O).
  92 rewrite > Hcut.
  93 simplify.fold simplify (m \sup (S n1)).
  94 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
  95 rewrite > Hcut1.
  96 rewrite > (H2 m1). simplify.reflexivity.
  97 apply le_S_S_to_le.assumption.
  98 (* div_exp *)
  99 simplify.
 100 rewrite > assoc_times.
 101 apply (lt_O_n_elim m H).
 102 intro.apply div_times.
 103 (* mod_exp = O *)
 104 apply divides_to_mod_O.
 105 assumption.
 106 simplify.rewrite > assoc_times.
 107 apply (witness ? ? (m \sup n1 *n)).reflexivity.
 108 qed.
 109
 110 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
 111   match p_ord_aux p n m with
 112   [ (pair q r) \Rightarrow r \mod m \neq O].
 113 intro.elim p.absurd (O < n).assumption.
 114 apply le_to_not_lt.assumption.
 115 simplify.
 116 apply (nat_case1 (n1 \mod m)).intro.
 117 generalize in match (H (n1 / m) m).
 118 elim (p_ord_aux n (n1 / m) m).
 119 apply H5.assumption.
 120 apply eq_mod_O_to_lt_O_div.
 121 apply (trans_lt ? (S O)).unfold lt.apply le_n.
 122 assumption.assumption.assumption.
 123 apply le_S_S_to_le.
 124 apply (trans_le ? n1).change with (n1 / m < n1).
 125 apply lt_div_n_m_n.assumption.assumption.assumption.
 126 intros.simplify.
 127 rewrite > H4.
 128 unfold Not.intro.
 129 apply (not_eq_O_S m1).
 130 rewrite > H5.reflexivity.
 131 qed.
 132
 133 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
 134  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
 135 intros.
 136 change with
 137   match (pair nat nat q r) with
 138   [ (pair q r) \Rightarrow r \mod m \neq O].
 139 rewrite > H3.
 140 apply p_ord_aux_to_Prop1.
 141 assumption.assumption.assumption.
 142 qed.
 143
 144 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
 145 n = p \sup q * r \to p_ord n p = pair nat nat q r.
 146 intros.unfold p_ord.
 147 rewrite > H2.
 148 apply p_ord_exp
 149  [assumption
 150  |unfold.intro.apply H1.
 151   apply mod_O_to_divides[assumption|assumption]
 152  |apply (trans_le ? (p \sup q)).
 153   cut ((S O) \lt p).
 154   elim q.simplify.apply le_n_Sn.
 155   simplify.
 156   generalize in match H3.
 157   apply (nat_case n1).simplify.
 158   rewrite < times_n_SO.intro.assumption.
 159   intros.
 160   apply (trans_le ? (p*(S m))).
 161   apply (trans_le ? ((S (S O))*(S m))).
 162   simplify.rewrite > plus_n_Sm.
 163   rewrite < plus_n_O.
 164   apply le_plus_n.
 165   apply le_times_l.
 166   assumption.
 167   apply le_times_r.assumption.
 168   apply not_eq_to_le_to_lt.
 169   unfold.intro.apply H1.
 170   rewrite < H3.
 171   apply (witness ? r r ?).simplify.apply plus_n_O.
 172   assumption.
 173   rewrite > times_n_SO in \vdash (? % ?).
 174   apply le_times_r.
 175   change with (O \lt r).
 176   apply not_eq_to_le_to_lt.
 177   unfold.intro.
 178   apply H1.rewrite < H3.
 179   apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
 180   apply le_O_n.
 181   ]
 182 qed.
 183
 184 theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
 185 \lnot p \divides r \land n = p \sup q * r.
 186 intros.
 187 unfold p_ord in H2.
 188 split.unfold.intro.
 189 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
 190 apply le_n.symmetry.assumption.
 191 apply divides_to_mod_O.apply (trans_lt ? (S O)).
 192 unfold.apply le_n.assumption.assumption.
 193 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
 194 unfold.apply le_n.assumption.symmetry.assumption.
 195 qed.
 196
 197 theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.
 198  intros 2;
 199  cases n;
 200   [ cases p; simplify; intros; destruct H; split; reflexivity;
 201   | cases p;
 202      [ intros;
 203        simplify in H;
 204        destruct H
 205      | cases n2;
 206         [ intros;
 207           simplify in H;
 208           rewrite < minus_n_O in H;
 209           simplify in H;
 210           change in H:(? ? match % return ? with [_⇒?|_⇒?] ?) with (mod n1 (S O));
 211           rewrite > mod_SO in H;
 212           simplify in H;
 213           change in H:(? ? match ? ? (? %) ? return ? with [_⇒?] ?) with (div n1 (S O));
 214           rewrite > div_SO in H;
 215           simplify in H;
 216
 217           letin H1 ≝ (p_ord_aux_to_exp n1 (S n1) 1); clearbody H1;
 218           elim (p_ord_aux n1 (S n1) 1) in H H1 (q' r'); simplify in H H1;
 219           destruct H;
 220           lapply (H1 q' O (le_n ?) (refl_eq ? ?));
 221           rewrite < times_n_O in Hletin;
 222           destruct Hletin
 223         | intros;
 224           lapply (p_ord_to_exp1 ? ? ? ? ? ? H);
 225           [ apply le_S_S;
 226             apply le_S_S;
 227             apply le_O_n
 228           | apply le_S_S;
 229             apply le_O_n
 230           | cases Hletin;
 231             elim H1;
 232             apply (witness ? O O);
 233             rewrite < times_n_O;
 234             reflexivity]]]]
 235 qed.
 236
 237 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
 238 \to O \lt a \to O \lt b
 239 \to p_ord a p = pair nat nat qa ra
 240 \to p_ord b p = pair nat nat qb rb
 241 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
 242 intros.
 243 cut ((S O) \lt p).
 244 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
 245 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
 246 apply p_ord_exp1.
 247 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
 248 unfold.intro.
 249 elim (divides_times_to_divides ? ? ? H H9).
 250 apply (absurd ? ? H10 H5).
 251 apply (absurd ? ? H10 H7).
 252 (* REGRESSION *)
 253 rewrite > H6.
 254 rewrite > H8.
 255 autobatch paramodulation.
 256 unfold prime in H. elim H. assumption.
 257 qed.
 258
 259 theorem fst_p_ord_times: \forall p,a,b. prime p
 260 \to O \lt a \to O \lt b
 261 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
 262 intros.
 263 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
 264 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
 265 simplify.reflexivity.
 266 apply eq_pair_fst_snd.
 267 apply eq_pair_fst_snd.
 268 qed.
 269
 270 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
 271 intros.
 272 apply p_ord_exp1.
 273 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
 274 unfold.intro.
 275 apply (absurd ? ? H).
 276 apply le_to_not_lt.
 277 apply divides_to_le.unfold.apply le_n.assumption.
 278 rewrite < times_n_SO.
 279 apply exp_n_SO.
 280 qed.
 281
 282 (* p_ord and divides *)
 283 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
 284 O < n \to O < m \to prime p
 285 \to divides n m \to p_ord n p = pair ? ? a b \to
 286 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
 287 intros.
 288 cut (S O < p)
 289   [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
 290    lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
 291    elim Hletin. clear Hletin.
 292    elim Hletin1. clear Hletin1.
 293    rewrite > H9 in H3.
 294    split
 295     [apply (gcd_SO_to_divides_times_to_divides (exp p c))
 296       [elim (le_to_or_lt_eq ? ? (le_O_n b))
 297         [assumption
 298         |apply False_ind.
 299          apply (lt_to_not_eq O ? H).
 300          rewrite > H7.
 301          rewrite < H10.
 302          autobatch;assumption;
 303         ]
 304       |elim c
 305         [rewrite > sym_gcd.
 306          apply gcd_SO_n
 307         |simplify.
 308          apply eq_gcd_times_SO
 309           [apply lt_to_le.assumption
 310           |apply lt_O_exp.apply lt_to_le.assumption
 311           |rewrite > sym_gcd.
 312            (* hint non trova prime_to_gcd_SO e
 313               autobatch non chiude il goal *)
 314            apply prime_to_gcd_SO
 315             [assumption|assumption]
 316           |assumption
 317           ]
 318         ]
 319       |apply (trans_divides ? n)
 320         [apply (witness ? ? (exp p a)).
 321          rewrite > sym_times.
 322          assumption
 323         |assumption
 324         ]
 325       ]
 326     |apply (le_exp_to_le p)
 327       [assumption
 328       |apply divides_to_le
 329         [apply lt_O_exp.apply lt_to_le.assumption
 330         |apply (gcd_SO_to_divides_times_to_divides d)
 331           [apply lt_O_exp.apply lt_to_le.assumption
 332           |elim a
 333             [apply gcd_SO_n
 334             |simplify.rewrite < sym_gcd.
 335              apply eq_gcd_times_SO
 336               [apply lt_to_le.assumption
 337               |apply lt_O_exp.apply lt_to_le.assumption
 338               |rewrite > sym_gcd.
 339               (* hint non trova prime_to_gcd_SO e
 340                  autobatch non chiude il goal *)
 341                apply prime_to_gcd_SO
 342                 [assumption|assumption]
 343               |rewrite > sym_gcd. assumption
 344               ]
 345             ]
 346           |apply (trans_divides ? n)
 347             [apply (witness ? ? b).assumption
 348             |rewrite > sym_times.assumption
 349             ]
 350           ]
 351         ]
 352       ]
 353     ]
 354   |elim H2.assumption
 355   ]
 356 qed.
 357
 358 (* p_ord and primes *)
 359 theorem not_divides_to_p_ord_O: \forall n,i.
 360 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
 361 pair nat nat O n.
 362 intros.
 363 apply p_ord_exp1
 364   [apply lt_O_nth_prime_n
 365   |assumption
 366   |autobatch
 367   ]
 368 qed.
 369
 370 theorem p_ord_O_to_not_divides: \forall n,i,r.
 371 O < n \to
 372 p_ord n (nth_prime i) = pair nat nat O r
 373 \to Not (divides (nth_prime i) n).
 374 intros.
 375 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 376   [apply lt_SO_nth_prime_n
 377   |assumption
 378   |elim Hletin.
 379    simplify in H3.
 380    rewrite > H3.
 381    rewrite < plus_n_O.
 382    assumption
 383   ]
 384 qed.
 385
 386 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
 387   (S O) < n \to
 388   p_ord n (nth_prime p) = pair nat nat q r \to
 389   Not (r=O).
 390 intros.
 391 unfold.intro.
 392 cut (O < n)
 393   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 394     [apply lt_SO_nth_prime_n.
 395     |assumption
 396     |elim Hletin.
 397      apply (lt_to_not_eq ? ? Hcut).
 398      rewrite > H4.
 399      rewrite > H2.
 400      apply times_n_O
 401     ]
 402   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 403   ]
 404 qed.
 405
 406 definition ord :nat \to nat \to nat \def
 407 \lambda n,p. fst ? ? (p_ord n p).
 408
 409 definition ord_rem :nat \to nat \to nat \def
 410 \lambda n,p. snd ? ? (p_ord n p).
 411
 412 theorem divides_to_ord: \forall p,n,m:nat.
 413 O < n \to O < m \to prime p
 414 \to divides n m
 415 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
 416 intros.
 417 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
 418   [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 419   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 420   ]
 421 qed.
 422
 423 theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
 424 O < n \to O < m \to prime p \to divides n m \to
 425 divides (ord_rem n p) (ord_rem m p).
 426 intros.
 427 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 428 qed.
 429
 430 theorem divides_to_le_ord: \forall p,n,m:nat.
 431 O < n \to O < m \to prime p \to divides n m \to
 432 (ord n p) \le (ord m p).
 433 intros.
 434 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 435 qed.
 436
 437 theorem exp_ord: \forall p,n. (S O) \lt p
 438 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
 439 intros.
 440 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
 441   [assumption
 442   |assumption
 443   |assumption
 444   |unfold ord.unfold ord_rem.
 445    apply eq_pair_fst_snd
 446   ]
 447 qed.
 448
 449 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
 450 \to divides (ord_rem n p) n.
 451 intros.
 452 apply (witness ? ? (p \sup (ord n p))).
 453 rewrite > sym_times.
 454 apply exp_ord[assumption|assumption]
 455 qed.
 456
 457 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
 458 intros.
 459 elim (le_to_or_lt_eq O (ord_rem n p))
 460   [assumption
 461   |apply False_ind.
 462    apply (lt_to_not_eq ? ? H1).
 463    lapply (divides_ord_rem ? ? H H1).
 464    rewrite < H2 in Hletin.
 465    elim Hletin.
 466    rewrite > H3.
 467    reflexivity
 468   |apply le_O_n
 469   ]
 470 qed.
 471
 472 (* properties of ord e ord_rem *)
 473
 474 theorem ord_times: \forall p,m,n.O<m \to O<n \to prime p \to
 475 ord (m*n) p = ord m p+ord n p.
 476 intros.unfold ord.
 477 rewrite > (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p))
 478   [reflexivity
 479   |assumption
 480   |assumption
 481   |assumption
 482   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 483   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 484   ]
 485 qed.
 486
 487 theorem ord_exp: \forall p,m.S O < p \to
 488 ord (exp p m) p = m.
 489 intros.
 490 unfold ord.
 491 rewrite > (p_ord_exp1 p (exp p m) m (S O))
 492   [reflexivity
 493   |apply lt_to_le.assumption
 494   |intro.apply (lt_to_not_le ? ? H).
 495    apply divides_to_le
 496     [apply lt_O_S
 497     |assumption
 498     ]
 499   |apply times_n_SO
 500   ]
 501 qed.
 502
 503 theorem not_divides_to_ord_O:
 504 \forall p,m. prime p \to \lnot (divides p m) \to
 505 ord m p = O.
 506 intros.unfold ord.
 507 rewrite > (p_ord_exp1 p m O m)
 508   [reflexivity
 509   |apply prime_to_lt_O.assumption
 510   |assumption
 511   |simplify.apply plus_n_O
 512   ]
 513 qed.
 514
 515 theorem ord_O_to_not_divides:
 516 \forall p,m. O < m \to prime p \to ord m p = O \to
 517 \lnot (divides p m).
 518 intros.
 519 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
 520   [elim Hletin.
 521    rewrite > H4.
 522    rewrite > H2.
 523    rewrite > sym_times.
 524    rewrite < times_n_SO.
 525    assumption
 526   |apply prime_to_lt_SO.assumption
 527   |assumption
 528   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 529   ]
 530 qed.
 531
 532 theorem divides_to_not_ord_O:
 533 \forall p,m. O < m \to prime p \to divides p m \to
 534 \lnot(ord m p = O).
 535 intros.intro.
 536 apply (ord_O_to_not_divides ? ? H H1 H3).
 537 assumption.
 538 qed.
 539
 540 theorem not_ord_O_to_divides:
 541 \forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to
 542 divides p m.
 543 intros.
 544 rewrite > (exp_ord p) in ⊢ (? ? %)
 545   [apply (trans_divides ? (exp p (ord m p)))
 546     [generalize in match H2.
 547      cases (ord m p);intro
 548       [apply False_ind.apply H3.reflexivity
 549       |simplify.autobatch
 550       ]
 551     |autobatch
 552     ]
 553   |apply prime_to_lt_SO.
 554    assumption
 555   |assumption
 556   ]
 557 qed.
 558
 559 theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to
 560 \lnot (divides p (ord_rem m p)).
 561 intros.
 562 elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
 563   [assumption
 564   |assumption
 565   |assumption
 566   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 567   ]
 568 qed.
 569
 570 theorem ord_ord_rem: \forall p,q,m. O < m \to
 571 prime p \to prime q \to
 572 q < p \to ord (ord_rem m p) q = ord m q.
 573 intros.
 574 rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?))
 575   [rewrite > ord_times
 576     [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?))
 577       [reflexivity
 578       |assumption
 579       |intro.
 580        apply (lt_to_not_eq ? ? H3).
 581        apply (divides_exp_to_eq ? ? ? H2 H1 H4)
 582       ]
 583     |apply lt_O_exp.
 584      apply (ltn_to_ltO ? ? H3)
 585     |apply lt_O_ord_rem
 586       [elim H1.assumption
 587       |assumption
 588
 589       ]
 590     |assumption
 591     ]
 592   |elim H1.assumption
 593   |assumption
 594   ]
 595 qed.
 596
 597 theorem lt_ord_rem: \forall n,m. prime n \to O < m \to
 598 divides n m \to ord_rem m n < m.
 599 intros.
 600 elim (le_to_or_lt_eq (ord_rem m n) m)
 601   [assumption
 602   |apply False_ind.
 603    apply (ord_O_to_not_divides ? ? H1 H ? H2).
 604    apply (inj_exp_r n)
 605     [apply prime_to_lt_SO.assumption
 606     |apply (inj_times_l1 m)
 607       [assumption
 608       |rewrite > sym_times in ⊢ (? ? ? %).
 609        rewrite < times_n_SO.
 610        rewrite < H3 in ⊢ (? ? (? ? %) ?).
 611        apply sym_eq.
 612        apply exp_ord
 613         [apply prime_to_lt_SO.assumption
 614         |assumption
 615         ]
 616       ]
 617     ]
 618   |apply divides_to_le
 619     [assumption
 620     |apply divides_ord_rem
 621       [apply prime_to_lt_SO.assumption
 622       |assumption
 623       ]
 624     ]
 625   ]
 626 qed.
 627
 628 (* p_ord_inv is used to encode the pair ord and rem into
 629    a single natural number. *)
 630
 631 definition p_ord_inv \def
 632 \lambda p,m,x.
 633   match p_ord x p with
 634   [pair q r \Rightarrow r*m+q].
 635
 636 theorem  eq_p_ord_inv: \forall p,m,x.
 637 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
 638 intros.unfold p_ord_inv. unfold ord_rem.
 639 unfold ord.
 640 elim (p_ord x p).
 641 reflexivity.
 642 qed.
 643
 644 theorem div_p_ord_inv:
 645 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
 646 intros.rewrite > eq_p_ord_inv.
 647 apply div_plus_times.
 648 assumption.
 649 qed.
 650
 651 theorem mod_p_ord_inv:
 652 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
 653 intros.rewrite > eq_p_ord_inv.
 654 apply mod_plus_times.
 655 assumption.
 656 qed.