The Nat (N ...) plus another Nat (N ...). Give the added value twice as a tuple.

nat6 |> NNat.add ( nat5, nat5 )
--> Nat 11
--> : Nat
-->     (N Nat11
-->         (Nat11Plus a)
-->         (Is a To Nat11Plus a)
-->         (Is b To Nat11Plus b)
-->     )

This is only rarely useful, as you shouldn't

inRangeXAndXPlus10 x =
    -- won't work
    isInRange x (x |> NNat.add ( nat10, nat10 ))


isAtLeast10GreaterThan x =
    -- the only use case
    isAtLeast (x |> NNat.add ( nat10, nat10 ))

(examples don't compile, just for demonstration)

The Nat (N ...) plus another Nat (N ...). Give the subtracted value twice as a tuple.

nat6 |> NNat.sub ( nat5, nat5 )
--> Nat 1
--> : Nat
-->     (N Nat1 (Nat1Plus orMore_)
-->         (Is a To (Nat1Plus a))
-->         (Is b To (Nat1Plus b))
-->     )

This is only rarely useful, as you shouldn't

inRangeXMinus10ToX x =
    -- won't work
    isInRange (x |> NNat.sub ( nat10, nat10 )) x


isAtLeast10LessThan x =
    -- the only use case
    isAtLeast (x |> NNat.sub ( nat10, nat10 ))

(examples don't compile, just for demonstration)