Library rt.util.induction

Require Import rt.util.tactics.

(* Induction lemmas for natural numbers. *)
Section NatInduction.

  Lemma strong_ind :
    ∀ (P: nat → Prop),
      (∀ n, (∀ k, k < n → P k) → P n) →
      ∀ n, P n.

  Lemma leq_as_delta :
    ∀ x1 (P: nat → Prop),
      (∀ x2, x1 ≤ x2 → P x2) ↔
      (∀ delta, P (x1 + delta)).

End NatInduction.