Search code examples
coqssreflect

using addf_div for rat_numDomainType

I am trying to apply the addf_div theorem from math-comp's ssralg to the following:

1 / a%:R + 1 / a%:R. I want to show that this is 2 / a%:R, but addf_div is over fieldTypes and can't be applied. Is there a way to apply addf_div to the goal.

Here, a is a nat.

Solution

  • I'm not at all an expert with ssralg, but I managed to get this direct proof, which I'm pretty sure can be very simplified.

    From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import GRing.Theory.

Variable (R : numFieldType).

Variable (a : nat).

Definition a' : R := a%:R.

Lemma foo : 1 / a' + 1 / a' = 2%:R / a'.
Proof. by rewrite -mulrDr -mulr2n mulrnAr -mulrnAl. Qed.

    Note that addf_div can be used inside the proof too, but using it doesn't seem to be making the proof simpler.