Induction proof
From Event-B
This page explains how to proove with induction method on the natural number with Rodin tools.
In other words, how to proove :
The proof key is the following theorem:
<math>
\forall s.s \subseteq \mathbb{N} \land 0 \in s \land (\forall n.n \in s => n+1 \in s)\Rightarrow N \subseteq s