The Coq mailing list

["Ly Kim Quyen (Gwenhael)" <lykimq AT gmail.com>]

Dear Club,

I have these code: 

Require Import Bool VecUtil ZArith ListForall List.  (*VecUtil and ListForall are the library in CoLoR project (http://color.inria.fr/doc/main.html) *)

Notation monom := (vector nat).

Definition poly n := list (Z * monom n).

Open Local Scope Z_scope.

Definition is_not_neg z :=
  match z with
    | Zneg _ => false
    | _ => true

  end.

Definition coef_pos n (p : poly n) := lforall (fun x => 0 <= fst x) p.

Definition bcoef_pos n (p : poly n) := forallb (fun x => is_not_neg (fst x)) p.

Lemma bcoef_pos_ok : forall n (p : poly n), bcoef_pos n p = true <-> coef_pos n p.

Proof.
Admitted.

Lemma bcoef_pos_ok_2 : forall n (p : poly n), bcoef_pos n p = true -> coef_pos n p.
Proof.
Admitted.

Record poly_mon n : Type := Build_poly_mon
      { p_poly : poly n; 
        pweak_mon_check : coef_pos n p_poly

      }.

Definition check n p : poly_mon n :=
  match bool_dec (bcoef_pos n p) true with
    | left h => Build_poly_mon n p (bcoef_pos_ok n p h)
    | right _ => _ (* whatever *)
  end.

My question is: Why I cannot apply the lemma bcoef_pos_ok in this definition? 
I got the error saying that: "The _expression_ "bcoef_pos_ok n p" of type  "bcoef_pos n p = true <-> coef_pos n p"

cannot be applied to the term  "h0" : "bcoef_pos n p = true" "
But if I am using the lemma bcoef_pos_ok_2 it works. 

Thank you very much,
Gwen