On 02/11/2019 19:10, Rob Arthan wrote:
If I need to work with the rationals I just treat
them as a subset of the reals.
Though I think for these examples even that is an unnecessary
complication, since the proof over the reals as a whole will be closest
(apart from the actual types) to what a proof for the rationals would
look like.
And the original seems ambiguous about types.
Roger
PS: my 0 < r < 1 suggestion seems unnecessary.
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
