X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=7dd4fb362bce6a7803caf1837ec2430e6370ddf2;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=335550d0d6366f02d172c1f3aa6171d3ef6d171a;hpb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;p=helm.git

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index 335550d0d..7dd4fb362 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/ord".
-
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/nth_prime.ma".
@@ -196,6 +194,46 @@ apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
 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  
@@ -211,8 +249,9 @@ unfold.intro.
 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.
@@ -260,7 +299,7 @@ cut (S O < p)
          apply (lt_to_not_eq O ? H).
          rewrite > H7.
          rewrite < H10.
-         autobatch
+         autobatch;assumption;
         ]
       |elim c
         [rewrite > sym_gcd.