proposition: Lemma eqb_false (A:Type) (x y:A) (eqb:A->A->bool) (eqb_spec : forall x y, if eqb x y then x = y else x <> y) (P:eqb x y = false) : x <> y.
proof: Proof. generalize (eqb_spec x y); intro H. destruct (eqb x y). discriminate P. assumption. Qed.