Library rt.util.exists

Require Import rt.util.tactics.

(* Lemmas about the finite existential for Ordinals: ∃ x, P x. *)
Section OrdExists.

  Lemma exists_ord0:
    ∀ (T: eqType) P,
      [∃ x in 'I_0, P x] = false.

  Lemma exists_recr:
    ∀ (T: eqType) n P,
      [∃ x in 'I_n.+1, P x] =
      [∃ x in 'I_n, P (widen_ord (leqnSn n) x)] || P (ord_max).

End OrdExists.