X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=340e33a865fb809d8beb35e632f4e129fa2bd0dc;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=4fd2fd2828bdd75616596a093d6f063339bd004c;hpb=a180bddcd4a8f35de3d7292162ba05d0077723aa;p=helm.git diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 4fd2fd282..340e33a86 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/nat/ord". include "datatypes/constructors.ma". include "nat/exp.ma". -include "nat/gcd.ma". +include "nat/nth_prime.ma". include "nat/relevant_equations.ma". (* required by autobatch paramod *) let rec p_ord_aux p n m \def @@ -166,8 +166,7 @@ apply p_ord_exp apply le_times_l. assumption. apply le_times_r.assumption. -alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". -apply not_eq_to_le_to_lt. + apply not_eq_to_le_to_lt. unfold.intro.apply H1. rewrite < H3. apply (witness ? r r ?).simplify.apply plus_n_O. @@ -240,6 +239,7 @@ rewrite < times_n_SO. apply exp_n_SO. qed. +(* p_ord and divides *) theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. O < n \to O < m \to prime p \to divides n m \to p_ord n p = pair ? ? a b \to @@ -313,7 +313,55 @@ cut (S O < p) ] |elim H2.assumption ] -qed. +qed. + +(* p_ord and primes *) +theorem not_divides_to_p_ord_O: \forall n,i. +Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = +pair nat nat O n. +intros. +apply p_ord_exp1 + [apply lt_O_nth_prime_n + |assumption + |autobatch + ] +qed. + +theorem p_ord_O_to_not_divides: \forall n,i,r. +O < n \to +p_ord n (nth_prime i) = pair nat nat O r +\to Not (divides (nth_prime i) n). +intros. +lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n + |assumption + |elim Hletin. + simplify in H3. + rewrite > H3. + rewrite < plus_n_O. + assumption + ] +qed. + +theorem p_ord_to_not_eq_O : \forall n,p,q,r. + (S O) < n \to + p_ord n (nth_prime p) = pair nat nat q r \to + Not (r=O). +intros. +unfold.intro. +cut (O < n) + [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1) + [apply lt_SO_nth_prime_n. + |assumption + |elim Hletin. + apply (lt_to_not_eq ? ? Hcut). + rewrite > H4. + rewrite > H2. + apply times_n_O + ] + |apply (trans_lt ? (S O))[apply lt_O_S|assumption] + ] +qed. definition ord :nat \to nat \to nat \def \lambda n,p. fst ? ? (p_ord n p). @@ -407,4 +455,4 @@ theorem mod_p_ord_inv: intros.rewrite > eq_p_ord_inv. apply mod_plus_times. assumption. -qed. \ No newline at end of file +qed.