Backward chaining

 A : Type
  k : nat
  O : (A -> bool) -> A -> bool
  Hmon : mon O
  l : list A
  Hin : forall a : A, In a l
  Hlen : length l <= k
  a : A
  m : nat
  H : iter O (S m) nil_pred a = true
  Hl : forall a : A, iter O k nil_pred a = true <-> iter O (k + 1) nil_pred a = true
  Hlel : S k <= m
  Hinc : forall (n : nat) (a : A), iter O n nil_pred a = true -> iter O (n + 1) nil_pred a = true
  IHHlel : iter O m nil_pred a = true -> iter O k nil_pred a = true
  ============================
  iter O k nil_pred a = true


  Theorem iter_fin {A: Type} (k: nat) (O: (A -> bool) -> (A -> bool)) :
    mon O -> bounded_card A k ->
    forall n: nat, forall a: A, iter O n nil_pred a = true -> iter O k nil_pred a = true.
  Proof.
    
    intros Hmon Hboun; unfold bounded_card in Hboun.
    destruct Hboun as [l [Hin Hlen]]. intros n a H.
    destruct (iter_aux_newagain O l Hmon Hin k) as [Hl | Hr]; swap 1 2.

    (*   Hr : card l (iter O (k + 1) nil_pred) >= k + 1 *)
    unfold card in Hr. specialize (length_filter A (iter O (plus k 1) nil_pred) l).
    intros Hl. omega.

    (*   Hl : forall a : A, iter O k nil_pred a = true <-> iter O (k + 1) nil_pred a = true *)
    assert (Hle : k < n \/ k >= n) by omega.    
    destruct Hle as [Hlel | Hler]; swap 1 2.
    (* k >= n *)
    clear Hlen; clear Hl.
    specialize (increasing O Hmon); intros Hinc; unfold pred_subset in Hinc.
    induction Hler. auto. specialize (Hinc m). replace (S m) with (plus m 1).
    apply Hinc. auto. omega.

    (* k < n *)
    specialize (increasing O Hmon); intros Hinc; unfold pred_subset in Hinc.   
    induction Hlel.
    (* base case of induction *)
    destruct (Hl a) as [Hlf Hlb]. replace (plus k 1) with (S k) in Hlb.
    apply Hlb in H. assumption. omega.
    (* not base case *)