New lemma

theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index ab5f8a52aa87f5504d2b3950c3989653fd167aa0..9d700714585569cb3705be2bb1682ef0148ea7a6 100644 (file)
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -194,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