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