+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.
+