<div dir="ltr">So it turns out the proposed definition of _+_ in the PR wasn't great. I'm just about to update the definition in the PR to remove the use of `with`. That should make it _much_ easier to work with. <div><br></div><div>You then basically have to prove that the numerator is positive. The difficult part of the proof will be showing that `norm-mkℚ` preserves the positiveness of the numerator. Let me know if you get stuck further.</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 23, 2018 at 5:28 PM Zambonifofex <<a href="mailto:zambonifofex@gmail.com">zambonifofex@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello, everyone! Kinda of a newbie question, but I am writing a game<br>
in Agda, and I’ve become stuck trying to get a specific proof.<br>
<br>
I have been working with the definitions found in<br>
‘agda/agda-stdlib#380’ on GitHub.<br>
<br>
So, I have two rationals, ‘a’ and ‘b’, proofs that they are both<br>
nonnegative, as well as a proof ‘b≤a : b ≤ a’. With the definition for<br>
‘_-_’ in the aforementioned pull request, is it possible to get a<br>
proof that ‘a - b’ is also nonnegative?<br>
<br>
Thank you all for your attention, and I am looking forward to sharing<br>
my finished game with you!<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>