Stream: math-comp users

Topic: ✔ Awful proof on rationals


view this post on Zulip Julien Puydt (May 25 2022 at 20:17):

Eh, it turns out the result I needed was a bit stronger than the simple case I asked about ; I was still able to adapt it, so here is what I turned up with:

Let only_positive_root: forall a: RR, (a == -1) || (a == 1 / 2%:R) -> (0 < a) -> a == 1 / 2%:R.
Proof.
move=> a /orP[] /eqP -> //. (* this one line works for a: rat *)
by rewrite Num.Theory.ltr0N1.
Qed.

where Definition RR := { realclosure rat }., coming from MC-real-closed.

@Pierre Roux Thanks!

view this post on Zulip Notification Bot (May 25 2022 at 20:17):

Julien Puydt has marked this topic as resolved.

view this post on Zulip Pierre Roux (May 25 2022 at 20:25):

Indeed, if a is not of a "concrete" type like rat, 0 < -1 cannot be simplified to false. Note that we often Import Num.Theory to avoid typing it again and again.


Last updated: Feb 08 2023 at 07:02 UTC