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.