Basics of real numbers in mathcomp (Coq)

Question

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?

Answer 1

Assuming you have opened ring_scope, for instance with

Local Open Scope ring_scope.

you can use 2%:R to mean the constant 2 in a ring instead of nat (or use MathComp >= 1.15.0 where 2 should work).

Answer 2

This should work:

From mathcomp Require Import all_ssreflect all_algebra ssralg ssrint ssrnum.
From mathcomp.analysis Require Import reals.
From mathcomp.algebra_tactics Require Import ring.

Variable R: realType.

Definition add_two_and_a_half (x : R) : R := x + (2 + 1/2).

Lemma six_and_two_and_a_half_make_eight_and_a_half : add_two_and_a_half 6 = (8 + 1/2)%R.
Proof.
 unfold add_two_and_a_half.
 by ring.
Qed.