The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello,

2012/4/5 gallais @ ensl.org 
<guillaume.allais AT ens-lyon.org>:
> In the stdlib, there is a theorem doing exactly what
> you are looking for:
>
> Rlt_not_eq
>     : forall r1 r2 : R, (r1 < r2)%R -> r1 <> r2

Thank you for pointing it out! I tried to use search features to look
for relevant theorems but overlooked this one.

In fact, theorem Rgt_not_eq is needed in my case.

Theorem b_div_b_is_one_2 : forall (b:R), (0%R <  b)%R -> (1%R = (Rdiv b b)%R).
intros.
field.
apply Rgt_not_eq.
assumption.
Qed.



BTW, is there a way in ProofGeneral to look for theorems having
notation like "<>" or "/"? For "<>", I had to search for Rdiv.

I tried [Search <>] or [Search "<>"] but it failed. I assume I need
some kind of "helper" for this specific notation?

"""
Toplevel input, characters 27-29:
> Search <>.
>        ^^
Syntax error: [constr:constr_pattern] expected after 'Search' (in
[vernac:command]).
"""

However [Print "<"] works.

Best regards,
d.