]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/library/nat/ord.ma
advances non lfsx ...
[helm.git] / matitaB / 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.