The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

On Mon, Jul 25, 2011 at 9:38 AM, Jean-Francois Monin
<jean-francois.monin AT imag.fr>
 wrote:
> Because A <-> B, by definition, is A -> B /\ B-> A.
> f : A -> B can be applied to an argument x:A,
> g: A <-> B cannot, only (fst g) can.

The confusion might come from the fact that when using tactics, and in
particular the "apply" tactics, the iff (<->) is implicitly converted
to either of its directions. For example, "apply bcoef_pos_ok" would
have worked on the goal "coef_pos n p", yielding the subgoal
"bcoef_pos n p = true". The same does not apply when writing proof
terms directly.

Cheers,
-- 
David