(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/ord".
-
include "datatypes/constructors.ma".
include "nat/exp.ma".
include "nat/nth_prime.ma".
unfold.apply le_n.assumption.symmetry.assumption.
qed.
+theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.
+ intros 2;
+ cases n;
+ [ cases p; simplify; intros; destruct H; split; reflexivity;
+ | cases p;
+ [ intros;
+ simplify in H;
+ destruct H
+ | cases n2;
+ [ intros;
+ simplify in H;
+ rewrite < minus_n_O in H;
+ simplify in H;
+ change in H:(? ? match % return ? with [_⇒?|_⇒?] ?) with (mod n1 (S O));
+ rewrite > mod_SO in H;
+ simplify in H;
+ change in H:(? ? match ? ? (? %) ? return ? with [_⇒?] ?) with (div n1 (S O));
+ rewrite > div_SO in H;
+ simplify in H;
+
+ letin H1 ≝ (p_ord_aux_to_exp n1 (S n1) 1); clearbody H1;
+ elim (p_ord_aux n1 (S n1) 1) in H H1 (q' r'); simplify in H H1;
+ destruct H;
+ lapply (H1 q' O (le_n ?) (refl_eq ? ?));
+ rewrite < times_n_O in Hletin;
+ destruct Hletin
+ | intros;
+ lapply (p_ord_to_exp1 ? ? ? ? ? ? H);
+ [ apply le_S_S;
+ apply le_S_S;
+ apply le_O_n
+ | apply le_S_S;
+ apply le_O_n
+ | cases Hletin;
+ elim H1;
+ apply (witness ? O O);
+ rewrite < times_n_O;
+ reflexivity]]]]
+qed.
+
theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
\to O \lt a \to O \lt b
\to p_ord a p = pair nat nat qa ra
elim (divides_times_to_divides ? ? ? H H9).
apply (absurd ? ? H10 H5).
apply (absurd ? ? H10 H7).
-(* rewrite > H6.
-rewrite > H8. *)
+(* REGRESSION *)
+rewrite > H6.
+rewrite > H8.
autobatch paramodulation.
unfold prime in H. elim H. assumption.
qed.
apply (lt_to_not_eq O ? H).
rewrite > H7.
rewrite < H10.
- autobatch
+ autobatch;assumption;
]
|elim c
[rewrite > sym_gcd.