The Coq mailing list

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

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