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

[Zambonifofex]

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!

[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.

Post by Zambonifofex
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
https://lists.chalmers.se/mailman/listinfo/agda