antitrue : so False -> a
antitrue oh impossible

total
prf : (a:Nat) -> (b:Nat) -> so (a > b) -> GT a b
prf Z     Z     oh impossible
prf Z     (S k) um = antitrue um
prf (S k) Z     um = lteSucc lteZero 
-- prf (S _) (S _) oh impossible