[Agda] Newbie question: For nonnegative rationals ‘a’ and ‘b’, how to prove ‘a - b’ is nonnegative, given that ‘b ≤ a’?

[Matthew Daggitt]

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.

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.

On Mon, Jul 23, 2018 at 5:28 PM Zambonifofex <zambonifofex at gmail.com> wrote:

> Hello, everyone! Kinda of a newbie question, but I am writing a game
> in Agda, and I’ve become stuck trying to get a specific proof.
>
> I have been working with the definitions found in
> ‘agda/agda-stdlib#380’ on GitHub.
>
> So, I have two rationals, ‘a’ and ‘b’, proofs that they are both
> nonnegative, as well as a proof ‘b≤a : b ≤ a’. With the definition for
> ‘_-_’ in the aforementioned pull request, is it possible to get a
> proof that ‘a - b’ is also nonnegative?
>
> Thank you all for your attention, and I am looking forward to sharing
> my finished game with you!
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180802/f3bc03a4/attachment.html>