Trivial lemma on real numbers on Coq

Question

I want to prove following lemma.

Require Import Reals.Reals.
Open Scope R_scope.

Lemma trivial_lemma (r1 r2:R) : r1 - (r1 - r2) = r2.
Proof.
rewrite <- Ropp_minus_distr.
rewrite Ropp_plus_distr.
rewrite Ropp_involutive.
rewrite Ropp_minus_distr'.
Abort.

I know Rplus_opp_l, but I cannot apply it to my goal because of r2.

Please tell me your solution.

Answer 1

First you should know that the automatic tactic ring solves this kind of goals autommatically. In the long run, you should rely on this tactic often if you wish to be productive.

Second, it appears (through Search) that the library does not contain many lemmas about subtraction. In this case, you may have to unfold this operator to end up with a goal that has the more primitive addition and opposite operations. Here is a sequence of rewrites that does your work.

unfold Rminus.
rewrite Ropp_plus_distr.  
rewrite Ropp_involutive.
rewrite <- Rplus_assoc.
rewrite Rplus_opp_r.
rewrite Rplus_0_l.
easy.

The fact that the library does not contain basic lemmas like this is an indication that the library designers intend users to rely more on the ring tactic.