Here you can infer that the type of 'a' inside the 'then' is a NonZeroNumber. "All" you need is for the type checker to be able to recognize when a conditional acts as a guard against a subset of the possible types.
But if we're dividing by (a-1) then recognizing that it's safe may require a type NonOneNumber. And in other cases perhaps NonFortyTwoNumber. Where does that end?
Only in as much as it would require the type checker to be able to express and operate on expressions constraining or combining types, not name every one. E.g. being able to recognise that in this:
if a < 2 then exit
.. afterward, "a" has a named numeric type fully covered by its previous type combined with the extra constraints of the check if that allows picking a more constrained type, and its real type is further constrained to the subset a>=2, and be able to reconcile that this means 'a' can't be 1.
In practice, yes, you can absolutely get into situations where this will mean you end up writing extra checks to prove to the compiler that a value can only be within the required subset if the type checker couldn't figure it out. How often will depend on how advanced your type checker is.
