The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I recently started using reals instead of integers in some proofs. Some of the
proofs are quite similar to those with integer arithmetic, and with the help 
of
[SearchPattern] and others, I could solve most so far.

However, I'm having most of my problems no with the (normally) very easy 
cases:
Here are some examples:

  forall (x : Z), 1 <= x -> x <> 0.
  forall (x : Z), 1 <= x -> x > 0.
  (2 <> 0).

I could easily solve all these proofs, either with [intuition] or [auto with
zarith]. The same proofs on reals, though, make much more problems:

  forall (x : R), (1 <= x)%R -> (x <> 0)%R.
  forall (x : R), (1 <= x)%R -> (x > 0)%R.
  (2 <> 0)%R.

Using [intuition] places the current goal as a hypothesis, and replace it with
the goal "False". [auto with zarith] of couse doesn't work either.

Is there a similar automatic way to solve those simple goals (auto with rarith
doesn't work), or, if not, what's the best approach to solve them.
SearchPattern didn't give me any useful Lemma (probably since they're so
trivial).

Sincerely,