Library prosa.classic.util.induction

Require Import prosa.classic.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* 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.