How do I talk about a particular constructor in Agda

Question

Say I have

data Maybe : Set -> Set where
    Just : forall {A} -> A -> Maybe A
    Nothing : forall {A} -> Maybe A

and I define my own minus like

minus : Nat -> Nat -> Maybe Nat
minus zero zero       = Just zero
minus zero _          = Nothing
minus n zero          = Just n
minus (suc n) (suc m) = minus n m

and I would like to prove that forall m n, if m > n, (minus m n) always spits out a (Just Nat). I am wondering how I can encode this claim in a type.

Thank you!

Answer 1

You can use the standard library's Is-just. Your statement will look like:

lt-minus-total : ∀ n m → m < n → Is-just (minus n m)