From: Wilmer Ricciotti Date: Tue, 25 Mar 2008 13:52:29 +0000 (+0000) Subject: small update X-Git-Tag: make_still_working~5500 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b771a37f83637be22d9b3f1254a6a0f15dc49612;p=helm.git small update --- diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma index b16eed5fa..628a91f10 100644 --- a/helm/software/matita/library/nat/bertrand.ma +++ b/helm/software/matita/library/nat/bertrand.ma @@ -236,16 +236,14 @@ intro.elim t 0 elim (in_list_cons_case ? ? ? ? H19) [rewrite > H20;apply le_n |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]] - |unfold;apply (ex_intro ? ? []); - apply (ex_intro ? ? l); - reflexivity] + |apply in_list_head] |elim (H3 t1);elim H11 [elim H13;apply lt_to_le;assumption |apply in_list_head] |assumption]] |elim (H3 t1);elim H9 [elim H11;assumption - |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]] + |apply in_list_head]] |intros;elim (le_to_or_lt_eq t1 x) [assumption |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9); @@ -260,8 +258,7 @@ intro.elim t 0 [assumption |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]] |elim (decidable_eq_nat p t1) - [rewrite > H10;apply (ex_intro ? ? []);apply (ex_intro ? ? l1); - reflexivity + [rewrite > H10;apply in_list_head |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros; apply (trans_le ? t1) [elim (decidable_lt p t1) @@ -283,8 +280,7 @@ intro.elim t 0 [rewrite > Hletin2 in H18;elim (H11 H18); lapply (H23 t1) [elim (lt_to_not_le ? ? Hletin3 Hletin) - |apply (ex_intro ? ? []);apply (ex_intro ? ? l); - reflexivity] + |apply in_list_head] |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18); elim H24;assumption]] |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]