The Coq mailing list

[Suneel Sarswat <suneel.sarswat AT gmail.com>]

I have a simple problem. I can't find any web link/document for this kind of situation. I have a record type r as

 Record r:=mkr { x: nat; xc: Nat.ltb x 5 = false}.

Now I want to write a function which takes a list ell of natural numbers and returns a list of type r as

 Fixpoint f (ell:list nat):(list r).
 refine ( match ell with
  |nil => nil
  |h::ell' => if Nat.ltb h 5 then f ell' else (mkr h _)::f ell'
end ).

The problem is it gives me a goal to prove "Nat.ltb h 5 = false" without the branch information or any condition on term h. In general how to extract branch information/pass dependent proof terms in a specific branch of function?

Thanks in advance. 

Regards,

Suneel