The Coq mailing list

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

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