The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

apply Lem1 in HW_0 did not do what I expected due to your hint.
My Proof is of the following form:
HW_0: a <= b * c / d
===============
apply Zdiv_le_lower_bound in HW_0.

Which results in the error message "Error: unable to unify".


Just to test whether I read something not correctly, i tried to apply the rule
to a "normal" proof, which works fine, so the Lemma seems to match.

assert (a <= b * c / d).
apply Zdiv_le_lower_bound.
======================
Subgoal 1: 0 <= b * c.
Subgoal 2: 0 < c.
Subgoal 3: a * c <= b * d.

What am I doing wrong then?