From: Stefano Zacchiroli Date: Wed, 26 Jul 2006 09:24:55 +0000 (+0000) Subject: added tinycals to the proof we frequently use for examples and screenshots X-Git-Tag: make_still_working~7007 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca8534777d87dd69765f5127dee5902631b06825;p=helm.git added tinycals to the proof we frequently use for examples and screenshots --- diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 715a9795f..e61658786 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -169,24 +169,23 @@ match f with | nfa_one \Rightarrow (S O) | (nfa_proper g) \Rightarrow defactorize_aux g O]. -theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat. -O < defactorize_aux f i. -intro.elim f.simplify.unfold lt. -rewrite > times_n_SO. -apply le_times. -change with (O < nth_prime i). -apply lt_O_nth_prime_n. -change with (O < exp (nth_prime i) n). -apply lt_O_exp. -apply lt_O_nth_prime_n. -simplify.unfold lt. -rewrite > times_n_SO. -apply le_times. -change with (O < exp (nth_prime i) n). -apply lt_O_exp. -apply lt_O_nth_prime_n. -change with (O < defactorize_aux n1 (S i)). -apply H. +theorem lt_O_defactorize_aux: + \forall f:nat_fact. + \forall i:nat. + O < defactorize_aux f i. +intro; elim f; +[1,2: + simplify; unfold lt; + rewrite > times_n_SO; + apply le_times; + [ change with (O < nth_prime i); + apply lt_O_nth_prime_n; + |2,3: + change with (O < exp (nth_prime i) n); + apply lt_O_exp; + apply lt_O_nth_prime_n; + | change with (O < defactorize_aux n1 (S i)); + apply H; ] ] qed. theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.