]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/ord.ma
...
[helm.git] / 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 (* rewrite > H6.
253 rewrite > H8. *)
254 autobatch paramodulation.
255 unfold prime in H. elim H. assumption.
256 qed.
257
258 theorem fst_p_ord_times: \forall p,a,b. prime p 
259 \to O \lt a \to O \lt b 
260 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
261 intros.
262 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
263 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
264 simplify.reflexivity.
265 apply eq_pair_fst_snd.
266 apply eq_pair_fst_snd.
267 qed.
268
269 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
270 intros.
271 apply p_ord_exp1.
272 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
273 unfold.intro.
274 apply (absurd ? ? H).
275 apply le_to_not_lt.
276 apply divides_to_le.unfold.apply le_n.assumption.
277 rewrite < times_n_SO.
278 apply exp_n_SO.
279 qed.
280
281 (* p_ord and divides *)
282 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. 
283 O < n \to O < m \to prime p 
284 \to divides n m \to p_ord n p = pair ? ? a b \to
285 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
286 intros.
287 cut (S O < p)
288   [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
289    lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
290    elim Hletin. clear Hletin.
291    elim Hletin1. clear Hletin1.
292    rewrite > H9 in H3.
293    split
294     [apply (gcd_SO_to_divides_times_to_divides (exp p c))
295       [elim (le_to_or_lt_eq ? ? (le_O_n b))
296         [assumption
297         |apply False_ind.
298          apply (lt_to_not_eq O ? H).
299          rewrite > H7.
300          rewrite < H10.
301          autobatch
302         ]
303       |elim c
304         [rewrite > sym_gcd.
305          apply gcd_SO_n
306         |simplify.
307          apply eq_gcd_times_SO
308           [apply lt_to_le.assumption
309           |apply lt_O_exp.apply lt_to_le.assumption
310           |rewrite > sym_gcd.
311            (* hint non trova prime_to_gcd_SO e
312               autobatch non chiude il goal *)
313            apply prime_to_gcd_SO
314             [assumption|assumption]
315           |assumption
316           ]
317         ]
318       |apply (trans_divides ? n)
319         [apply (witness ? ? (exp p a)).
320          rewrite > sym_times.
321          assumption
322         |assumption
323         ]
324       ]
325     |apply (le_exp_to_le p)
326       [assumption
327       |apply divides_to_le
328         [apply lt_O_exp.apply lt_to_le.assumption
329         |apply (gcd_SO_to_divides_times_to_divides d)
330           [apply lt_O_exp.apply lt_to_le.assumption
331           |elim a
332             [apply gcd_SO_n
333             |simplify.rewrite < sym_gcd.
334              apply eq_gcd_times_SO
335               [apply lt_to_le.assumption
336               |apply lt_O_exp.apply lt_to_le.assumption
337               |rewrite > sym_gcd.
338               (* hint non trova prime_to_gcd_SO e
339                  autobatch non chiude il goal *)
340                apply prime_to_gcd_SO
341                 [assumption|assumption]
342               |rewrite > sym_gcd. assumption
343               ]
344             ]
345           |apply (trans_divides ? n)
346             [apply (witness ? ? b).assumption
347             |rewrite > sym_times.assumption
348             ]
349           ]
350         ]
351       ]
352     ]
353   |elim H2.assumption
354   ]
355 qed.    
356
357 (* p_ord and primes *)
358 theorem not_divides_to_p_ord_O: \forall n,i.
359 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
360 pair nat nat O n.
361 intros.
362 apply p_ord_exp1
363   [apply lt_O_nth_prime_n
364   |assumption
365   |autobatch
366   ]
367 qed.
368
369 theorem p_ord_O_to_not_divides: \forall n,i,r.
370 O < n \to
371 p_ord n (nth_prime i) = pair nat nat O r 
372 \to Not (divides (nth_prime i) n).
373 intros.
374 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
375   [apply lt_SO_nth_prime_n
376   |assumption
377   |elim Hletin.
378    simplify in H3.
379    rewrite > H3.
380    rewrite < plus_n_O.
381    assumption
382   ]
383 qed.
384
385 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
386   (S O) < n \to
387   p_ord n (nth_prime p) = pair nat nat q r \to
388   Not (r=O).
389 intros.
390 unfold.intro.
391 cut (O < n)
392   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
393     [apply lt_SO_nth_prime_n.
394     |assumption
395     |elim Hletin.
396      apply (lt_to_not_eq ? ? Hcut).
397      rewrite > H4.
398      rewrite > H2.
399      apply times_n_O
400     ]
401   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
402   ]
403 qed.
404
405 definition ord :nat \to nat \to nat \def
406 \lambda n,p. fst ? ? (p_ord n p).
407
408 definition ord_rem :nat \to nat \to nat \def
409 \lambda n,p. snd ? ? (p_ord n p).
410          
411 theorem divides_to_ord: \forall p,n,m:nat. 
412 O < n \to O < m \to prime p 
413 \to divides n m 
414 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).  
415 intros.
416 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
417   [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
418   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
419   ]
420 qed.
421
422 theorem divides_to_divides_ord_rem: \forall p,n,m:nat. 
423 O < n \to O < m \to prime p \to divides n m \to
424 divides (ord_rem n p) (ord_rem m p).
425 intros.
426 elim (divides_to_ord p n m H H1 H2 H3).assumption.
427 qed.
428
429 theorem divides_to_le_ord: \forall p,n,m:nat. 
430 O < n \to O < m \to prime p \to divides n m \to
431 (ord n p) \le (ord m p).  
432 intros.
433 elim (divides_to_ord p n m H H1 H2 H3).assumption.
434 qed.
435
436 theorem exp_ord: \forall p,n. (S O) \lt p 
437 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
438 intros.
439 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
440   [assumption
441   |assumption
442   |assumption
443   |unfold ord.unfold ord_rem.
444    apply eq_pair_fst_snd
445   ]
446 qed.
447
448 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n 
449 \to divides (ord_rem n p) n. 
450 intros.
451 apply (witness ? ? (p \sup (ord n p))).
452 rewrite > sym_times. 
453 apply exp_ord[assumption|assumption]
454 qed.
455
456 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p. 
457 intros.
458 elim (le_to_or_lt_eq O (ord_rem n p))
459   [assumption
460   |apply False_ind.
461    apply (lt_to_not_eq ? ? H1).
462    lapply (divides_ord_rem ? ? H H1).
463    rewrite < H2 in Hletin.
464    elim Hletin.
465    rewrite > H3.
466    reflexivity
467   |apply le_O_n
468   ]
469 qed.
470
471 (* properties of ord e ord_rem *)
472
473 theorem ord_times: \forall p,m,n.O<m \to O<n \to prime p \to
474 ord (m*n) p = ord m p+ord n p.
475 intros.unfold ord.
476 rewrite > (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p))
477   [reflexivity
478   |assumption
479   |assumption
480   |assumption
481   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
482   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
483   ]
484 qed.
485
486 theorem ord_exp: \forall p,m.S O < p \to
487 ord (exp p m) p = m.
488 intros.
489 unfold ord.
490 rewrite > (p_ord_exp1 p (exp p m) m (S O))
491   [reflexivity
492   |apply lt_to_le.assumption
493   |intro.apply (lt_to_not_le ? ? H).
494    apply divides_to_le
495     [apply lt_O_S
496     |assumption
497     ]
498   |apply times_n_SO
499   ]
500 qed.
501
502 theorem not_divides_to_ord_O: 
503 \forall p,m. prime p \to \lnot (divides p m) \to
504 ord m p = O.
505 intros.unfold ord.
506 rewrite > (p_ord_exp1 p m O m)
507   [reflexivity
508   |apply prime_to_lt_O.assumption
509   |assumption
510   |simplify.apply plus_n_O
511   ]
512 qed.
513
514 theorem ord_O_to_not_divides: 
515 \forall p,m. O < m \to prime p \to ord m p = O \to 
516 \lnot (divides p m).
517 intros.
518 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
519   [elim Hletin.
520    rewrite > H4.
521    rewrite > H2.
522    rewrite > sym_times.
523    rewrite < times_n_SO.
524    assumption
525   |apply prime_to_lt_SO.assumption
526   |assumption
527   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
528   ]
529 qed.
530
531 theorem divides_to_not_ord_O: 
532 \forall p,m. O < m \to prime p \to divides p m \to
533 \lnot(ord m p = O).
534 intros.intro.
535 apply (ord_O_to_not_divides ? ? H H1 H3).
536 assumption.
537 qed.
538
539 theorem not_ord_O_to_divides: 
540 \forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to 
541 divides p m.
542 intros.
543 rewrite > (exp_ord p) in ⊢ (? ? %)
544   [apply (trans_divides ? (exp p (ord m p)))
545     [generalize in match H2.
546      cases (ord m p);intro
547       [apply False_ind.apply H3.reflexivity
548       |simplify.autobatch
549       ]
550     |autobatch
551     ]
552   |apply prime_to_lt_SO.
553    assumption
554   |assumption
555   ]
556 qed.
557
558 theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to
559 \lnot (divides p (ord_rem m p)).
560 intros.
561 elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
562   [assumption
563   |assumption
564   |assumption
565   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
566   ]
567 qed.
568
569 theorem ord_ord_rem: \forall p,q,m. O < m \to 
570 prime p \to prime q \to
571 q < p \to ord (ord_rem m p) q = ord m q.
572 intros.
573 rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?))
574   [rewrite > ord_times
575     [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?))
576       [reflexivity
577       |assumption
578       |intro.
579        apply (lt_to_not_eq ? ? H3).
580        apply (divides_exp_to_eq ? ? ? H2 H1 H4)
581       ]
582     |apply lt_O_exp.
583      apply (ltn_to_ltO ? ? H3)
584     |apply lt_O_ord_rem
585       [elim H1.assumption
586       |assumption
587       
588       ]
589     |assumption
590     ]
591   |elim H1.assumption
592   |assumption
593   ]
594 qed.
595
596 theorem lt_ord_rem: \forall n,m. prime n \to O < m \to
597 divides n m \to ord_rem m n < m.
598 intros.
599 elim (le_to_or_lt_eq (ord_rem m n) m)
600   [assumption
601   |apply False_ind.
602    apply (ord_O_to_not_divides ? ? H1 H ? H2).
603    apply (inj_exp_r n)
604     [apply prime_to_lt_SO.assumption
605     |apply (inj_times_l1 m)
606       [assumption
607       |rewrite > sym_times in ⊢ (? ? ? %).
608        rewrite < times_n_SO.
609        rewrite < H3 in ⊢ (? ? (? ? %) ?).
610        apply sym_eq.
611        apply exp_ord
612         [apply prime_to_lt_SO.assumption
613         |assumption
614         ]
615       ]
616     ]
617   |apply divides_to_le
618     [assumption
619     |apply divides_ord_rem
620       [apply prime_to_lt_SO.assumption
621       |assumption
622       ]
623     ]
624   ]
625 qed.
626
627 (* p_ord_inv is used to encode the pair ord and rem into 
628    a single natural number. *)
629  
630 definition p_ord_inv \def
631 \lambda p,m,x.
632   match p_ord x p with
633   [pair q r \Rightarrow r*m+q].
634   
635 theorem  eq_p_ord_inv: \forall p,m,x.
636 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
637 intros.unfold p_ord_inv. unfold ord_rem.
638 unfold ord.
639 elim (p_ord x p).
640 reflexivity.
641 qed.
642
643 theorem div_p_ord_inv: 
644 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
645 intros.rewrite > eq_p_ord_inv.
646 apply div_plus_times.
647 assumption.
648 qed.
649
650 theorem mod_p_ord_inv: 
651 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
652 intros.rewrite > eq_p_ord_inv.
653 apply mod_plus_times.
654 assumption.
655 qed.