small update

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index b16eed5fafae1ebcc7015988758d1fb13b648587..628a91f10e09101560ab1c536771b2830e63c2a5 100644 (file)
--- 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]