The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I have such problem:
  Record R := { number : nat; proof : exists n, n + number = 100 }.

  Lemma r_eq (x y : R) : number x = number y -> x = y.

  Admitted.

Is it possible to solve it and how?

Sincerely,
Kirill Taran