The Coq mailing list

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

Hi Lucian,

You can also do something like this (that does not use fourier).

I guess that records are handled in a special way that allows

to use apply when you actually just want to apply one of the

projections.

Lemma nonnegreal_plus_posreal : forall (x : nonnegreal) (y : posreal),

  0 < x + y.

Proof.

  intros x y.

  apply Rplus_le_lt_0_compat.

  apply x.

  apply y.

Qed.

Cheers,

--
guillaume

On 29 July 2011 23:08, Lucian M. Patcas <lucian.patcas AT gmail.com> wrote:

For some reason I just didn't see the solution, but I have it figured out now:

Lemma nonnegreal_plus_posreal : forall (x : nonnegreal) (y : posreal),
  0 < x + y.
Proof.
  intros x y.
  destruct x.
  destruct y.

  simpl.
  fourier.
Qed.

On Fri, Jul 29, 2011 at 14:30, Lucian M. Patcas <lucian.patcas AT gmail.com> wrote:

Hello,

I don't know what to do about the records in the goal. Any suggestions?

Lemma nonnegreal_plus_posreal : forall (x : nonnegreal) (y : posreal),
  0 < x + y.
Proof.
  intros x y.
  destruct x.
  destruct y.

1 subgoal
 
  nonneg : R
  cond_nonneg : 0 <= nonneg
  pos : R
  cond_pos : 0 < pos
  ============================
   0 <=
   {| nonneg := nonneg; cond_nonneg := cond_nonneg |} +
   {| pos := pos; cond_pos := cond_pos |}

Thanks,
Lucian