minus, with erasue

gistfile1.txt

  module erase
  
  data LessThan : Nat -> Nat -> Type where
       LtO : LessThan Z (S k)
       LtS : LessThan x y -> LessThan (S x) (S y)
  
  minus : (x : Nat) -> (y : Nat) -> LessThan y x -> Nat
  minus (S k) Z LtO = S k
  minus (S k) (S j) (LtS z) = minus k j
  
And minus at run time look a bit like...

[{e0},{e1},{e2}] case {e1} of
    0 => prim__addBigInt {e0}!-1 1
    {e4}+1 => erase.minus {e0}!-1 {e4} [__]
        
(Sorry for the ugly syntax, that's just how Idris prints it... but, no proof! At least, not one the machine ever looks at.)