proposition: Theorem double_induction : (forall m, R 0 m) -> (forall n, R (S n) 0) -> (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m.
proof: Proof. intros H1 H2 H3 n; induct n; auto. intros n H m; cases m; auto. Qed.
imports: Decidable NAxioms NZProperties