That link only goes part way. What you'd need to do is something like createProof : (n : Nat) -> (m : Nat) -> Maybe (n >= m) which could either succeed o

That link only goes part way. What you'd need to do is something like createProof : (n : Nat) -> (m : Nat) -> Maybe (n >= m) which could either succeed or fail to produce the needed proof at runtime. Without the proof it'd be impossible to perform the subtraction, so that branch of your program is statically inaccessible.