X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=9d700714585569cb3705be2bb1682ef0148ea7a6;hb=8f4162a9db17a597d4fba49eb957009fc0268378;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..9d7007145 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