The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi David,

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

Cheers,

--
gallais



On 5 April 2012 08:31, David MENTRE 
<dmentre AT linux-france.org>
 wrote:
> Hello,
>
> I laboriously proved following two simple theorems on reals. I tried
> the [fourier] tactic without success. I thought it would help with
> following kind of sub-goal:
>
>  b : R
>  H : 0 < b
>  ============================
>   b <> 0
>
>
> Would readers of this list have suggestions on more efficient way to
> do those proofs?
>
> ===========
> Require Import Rbase.
> Require Import Fourier.
>
>
> Theorem b_div_b_is_one : forall (b:R), (0%R <  b)%R -> (1%R = (Rdiv b b)%R).
> intros.
> field.
> contradict H.
> rewrite H.
> apply Rlt_irrefl.
> Qed.
>
> Theorem perm_div2 : forall (a:R) (b:R), ((0%R <  a)%R /\ (0%R <  b)%R) ->
>  ((Rdiv (a * b)%R b)%R = ((Rdiv a b)%R * b)%R).
> intros.
> field.
> elim H.
> intros.
> contradict H1.
> rewrite H1.
> apply Rlt_irrefl.
> Qed.
> =================
>
> Sincerely yours,
> david