ATS Proof: Why does this static if need greater than or equal to?

I was writing a proof of a*0=0 and I stumbled on some strangeness. Why does the sif a >= 0 on line 7 need to be a >=, and does not compile when its just sif > 0?

prfn mul_ax0_0 {a:int} () : MUL(a,0,0) =
let
    prfun auxnat {a:nat} .<a>. () : MUL(a,0,0) =
        sif a == 0 then MULbas()
        else MULind(auxnat{a-1}())
in
    sif a >= 0 then auxnat{a}() // line 7
    else MULneg(auxnat{~a}())
end

implement main0 () = ()

Intuitively, the a=0 should be handled fine by either path, yet only the first path works. Why?