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.
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.Note that
addf_div
can be used inside the proof too, but using it doesn't seem to be making the proof simpler.