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

nat6 |> NNat.add ( nat5, nat5 )
--> Nat 11 :
--> Nat
-->     (ValueN 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
-->         (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)