Library hydras.Prelude.MoreDecidable

From Coq Require Export Decidable Arith Lia.

Remark boundedCheck :
 ∀ P : nat → Prop,
 (∀ x : nat, decidable (P x)) →
 ∀ c : nat,
 (∀ d : nat, d < c → ¬ P d) ∨ (∃ d : nat, d < c ∧ P d).

Remark smallestExists :
 ∀ P : nat → Prop,
 (∀ x : nat, decidable (P x)) →
 ∀ c : nat,
 P c → ∃ a : nat, P a ∧ (∀ b : nat, b < a → ¬ P b).