I'm trying to play around with the Mathematical Components library in Coq but am having trouble writing basic, concrete statements about real numbers. E.g., I'd like to define
Definition add_two_and_a_half (x : R) : R := x + (2 + 1/2).
and then prove
Lemma six_and_two_and_a_half_make_eight_and_a_half : add_two_and_a_half 6 = (8 + 1/2)%R.
This works fine if I use the Coq.Reals.Reals library, but once I introduce mathcomp the lemma no longer goes through. What are some ways I can make this work?