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