(prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
intro.elim t 0
[intros;cut (l2 = [])
- [|generalize in match H2;elim l2
+ [|elim l2 in H2 ⊢ %
[reflexivity
- |simplify in H6;elim (not_le_Sn_O ? H6)]]
+ |simplify in H5;elim (not_le_Sn_O ? H5)]]
simplify;split
[assumption
|intro;elim (H p);split;intros
lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
intros;elim H;simplify
[apply in_list_head
- |generalize in match H2;elim H1;simplify;apply in_list_head]
+ |elim H1 in H2 ⊢ %;simplify;apply in_list_head]
qed.
lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
intros;unfold list_n in H;lapply (le_list_n_aux ? ? ? H);
-simplify in Hletin;generalize in match H;generalize in match Hletin;elim m
- [simplify in H2;elim (not_in_list_nil ? ? H2)
- |simplify in H2;assumption]
+simplify in Hletin;elim m in H Hletin ⊢ %
+ [simplify in H;elim (not_in_list_nil ? ? H)
+ |simplify in H;assumption]
qed.
[intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
- |intros 5;simplify;generalize in match H2;elim H3
+ |intros 5;simplify;elim H3 in H2 ⊢ %
[apply in_list_head
- |apply in_list_cons;apply H6
+ |apply in_list_cons;apply H5
[apply le_S_S;assumption
- |rewrite < plus_n_Sm in H7;apply H7]]]
+ |rewrite < plus_n_Sm in H6;apply H6]]]
qed.
lemma le_list_n_r : \forall n,m.S O < m \to 2 \leq n \to n \leq m \to in_list ? n (list_n m).
intros;unfold list_n;apply le_list_n_aux_r
[elim H;simplify
[apply lt_O_S
- |generalize in match H4;elim H3;
+ |elim H3 in H4 ⊢ %;
[apply lt_O_S
|simplify in H7;apply le_S;assumption]]
|assumption
- |simplify;generalize in match H2;elim H;simplify;assumption]
-qed.
+ |simplify;elim H in H2 ⊢ %;simplify;assumption]
+qed.
lemma le_length_list_n : \forall n. length ? (list_n n) \leq n.
intro;cut (\forall n,k.length ? (list_n_aux n k) \leq (S n))