From 08fddf59ad83f95ece083c6434bbffee6d0d1ba8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 13 Jun 2008 09:07:16 +0000 Subject: [PATCH] =?utf8?q?New=20lemma=20theorem=20eq=5Fp=5Ford=5Fq=5FO:=20?= =?utf8?q?=E2=88=80p,n,q.=20p=5Ford=20n=20p=20=3D=20pair=20=3F=20=3F=20q?= =?utf8?q?=20O=20=E2=86=92=20n=3DO=20=E2=88=A7=20q=3DO.?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- helm/software/matita/library/nat/ord.ma | 40 +++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index ab5f8a52a..9d7007145 100644 --- 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 -- 2.39.2