How does one know what statements in Coq require Induction?
Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal.

Most of the time, people doing maths are not exposed to mathematical logic. They do not know, for instance, how to define the set of real numbers. Or even the set of natural numbers. Numeric sets are simply taken for granted, together with their operations and related properties. On top of these "basic facts" people build more complex theorems. Essentially, the "basic facts" are used as if they were axioms.

Note that one could work at a similar level in Coq, if one wishes. One can import the Arith Coq library, which provides the basic facts of arithmetics, and exploit those.

However, the underlying logic of Coq does not take those properties for granted. The type of natural numbers, for instance, is not a primitive concept in the logic, but rather something which is defined using induction. Since that makes nat an inductive type, virtually every proof about naturals will require induction. (This also holds in set theory, e.g. Zermelo-Fraenkel, where naturals are also defined in a sort-of inductive way.)

Arithmetical operators are also defined using induction. Using a simplified syntax, one could define multiplication as

x * 0     = 0
x * (S y) = x + (x * y)


or, alternatively,

0 * x     = 0
(S y) * x = x + (y * x)


Both definitions are equivalent. However, using the first one will result in us being able to prove x * 0 = 0 "without induction" -- it follows by definition. In Coq, we can simply write reflexivity and let the system expand the definition for us.

By comparison, 0 * x = 0 is not a trivial equation which follows from the definition: to expand the definition we need to know what is the second argument of the multiplication, but here it's merely an unknown x. Hence, for this we do need induction over x. There's no way around that.

Note that, if we used the second definition instead, we would prove 0 * x = 0 immediately, and instead require induction for x * 0 = 0. So, no definition is strictly better than the other one.