proposition: Theorem two_dim_induction : R 0 0 -> (forall n m, R n m -> R n (S m)) -> (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m.
proof: Proof. intros H1 H2 H3. intro n; induct n. - intro m; induct m. + exact H1. + exact (H2 0). - intros n IH. intro m; induct m. + now apply H3. + exact (H2 (S n)). Qed.
imports: Decidable NAxioms NZProperties