Chainofreasoning.v

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
  n : nat
  Hler : k >= n
  H : forall a : A, iter O k nil_pred a = true <-> iter O (k + 1) nil_pred a = true
  a : A
  Hiter : iter O n nil_pred a = true
  H0 : forall (n : nat) (a : A), iter O n nil_pred a = true -> iter O (n + 1) nil_pred a = true
  ============================
  iter O k nil_pred a = true
  
  From H0 and Hler, it is obvious that goal is true. How to follow this kind of chain of reasoning in Coq
  
  Complete source code. 
  https://github.com/mukeshtiwari/formalized-voting/blob/master/fp.v