remember.v

 Theorem  iter_fp_gfp {A: Type} (O: Op A) (l: list A):
    mon O -> (forall a: A, In a l) ->
    forall (n : nat), (pred_eeq (iter O (n + 1) full_ss) (iter O n full_ss)) \/
               (card l (iter O (n+1) full_ss) + (n + 1)) <= length l.
  Proof.
    intros Hmon Hfin n. induction n.
    destruct (iter_aux_dec O l Hmon Hfin 0).
    left. assumption.
    right. replace (0 + 1)%nat with 1 in *.
    transitivity (card l (iter O 0 full_ss))%nat.
    remember (card l (iter O 0 full_ss)) as a.
    remember (card l (iter O 1 full_ss)) as b.
    
    
     
  A : Type
  O : Op A
  l : list A
  Hmon : mon O
  Hfin : forall a : A, In a l
  H : card l (iter O 0 full_ss) >= card l (iter O 1 full_ss) + 1
  a : nat
  Heqa : a = card l (iter O 0 full_ss)
  b : nat
  Heqb : b = card l (iter O 1 full_ss)
  ============================
  b + 1 <= a