The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

I think I misunderstood something in the "direction" of my proof. When I apply
a Lemma to my proof, the proof has to match the "right side" and is replaced 
by
the left side (the precondition). When I apply the Lemma to a Hypothesis, the
Hypothesis has to match the left side of course. So, what I wanted to do
doesn't make sense.

I have another question then with my new proof. If I have a proof "x <= y", is
there a way to proof it by contradiction (something like creating a hypothesis
"x > y" and concluding "False")?