return to top
source
MORENIKEJI NERI THOMAS POWELL
We formalize the first example from the paper.
For the inequality to hold we do not need to use the type NNReal but can also use Real; and we can generalize c as well:
NNReal
Real
c