totality006.idr

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