Forall.v

 Theorem  iter_aux_new {A: Type} (O: (A -> bool) -> (A -> bool)) (l: list A):
    mon O ->
    (forall a: A, In a l) ->
    forall (n : nat), (forall a:A, iter O n nil_pred a = true <-> iter O (n+1) nil_pred a = true) \/
               card l (iter O n nil_pred) >= n.
  Proof.              
    intros Hmon Hfin n. specialize (iter_aux O l Hmon Hfin n); intros.
    destruct H as [H | H]. left. assumption.
    right. unfold mon in Hmon. unfold card in H; unfold card.
    generalize dependent n. 
    
  and goal is 
    
    
  A : Type
  O : (A -> bool) -> A -> bool
  l : list A
  Hmon : forall p1 p2 : A -> bool, pred_subset p1 p2 -> pred_subset (O p1) (O p2)
  Hfin : forall a : A, In a l
  ============================
  forall n : nat,
  length (filter (iter O (n + 1) nil_pred) l) >= length (filter (iter O n nil_pred) l) + 1 ->
  length (filter (iter O n nil_pred) l) >= n


    
    
    

Theorem iter_aux_new {A: Type} (O: (A -> bool) -> (A -> bool)) (l: list A):
mon O ->
(forall a: A, In a l) ->
forall (n : nat), (forall a:A, iter O n nil_pred a = true <-> iter O (n+1) nil_pred a = true) /
card l (iter O n nil_pred) >= n.
Proof.
intros Hmon Hfin n. specialize (iter_aux O l Hmon Hfin n); intros.
destruct H as [H | H]. left. assumption.
right. unfold mon in Hmon. unfold card in H; unfold card.
(* specialize (increasing O Hmon); intros Hinc.
unfold pred_subset in Hinc. *)
generalize dependent n. induction n.
intros. omega.
intros.

Goal is

A : Type
O : (A -> bool) -> A -> bool
l : list A
Hmon : forall p1 p2 : A -> bool, pred_subset p1 p2 -> pred_subset (O p1) (O p2)
Hfin : forall a : A, In a l
n : nat
IHn : length (filter (iter O (n + 1) nil_pred) l) >= length (filter (iter O n nil_pred) l) + 1 ->
length (filter (iter O n nil_pred) l) >= n
H : length (filter (iter O (S n + 1) nil_pred) l) >=
length (filter (iter O (S n) nil_pred) l) + 1

length (filter (iter O (S n) nil_pred) l) >= S n