The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction. The B proof rules for invariant preservation are an induction proof in disguise, but that is another story. They require coding your problem and induction steps as B operations. Here, I am interested in proving properties in B directly using induction. Can this be done at all, without resorting to provers such as Isabelle? The answer is, yes. The reason is that B is not just rooted in predicate logic, but has access to arithmetic and set theory. As such, induction comes ``bundled with the arithmetic operators and data types.