The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I've got a Lemma, stating that for every y of myType there's a corresponding
x:Z

Lem1:
  forall (y: myType),
  exists x : Z,
  (x = func1(y)),
Admitted.

Now in my proof, I've got some variables of myType in a formula, which I would
like to be replaced, e.g.:

func1(y0) * 3 <= func1(y0) * 4 + 3

Since Coq doesn't know much about func1, this can't be solved at first.
Therefore, I'd like to introduce a new variable according to Lem1, to change 
it
to

x0 * 3 <= x0 * 4 + 3.

How can I "apply" my Lemma Lem1 to the proof here?


Sincerely