The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

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