proposition: Lemma bounded_quantifier_informative : forall (N : nat) (phi psi : nat -> CProp), (forall m : nat, m <= N -> phi m or psi m) -> (forall m : nat, m <= N -> phi m) or {j : nat | Cle j N | psi j}.
proof: Proof. do 3 intro. intro H. induction N as [| N HrecN]. cut (phi 0 or psi 0). intro H0. case H0. intros. left. intros. rewrite (proj1 (Nat.le_0_r m) H1). assumption. intro. right. exists 0. constructor. assumption. apply H. constructor. case HrecN. intros. apply H. apply Nat.le_trans with (m := N). assumption. apply Nat.le_succ_diag_r. intro. case (H (S N)). apply le_n. intros. left. intros. case (le_lt_eq_dec m (S N)). assumption. intros. apply p. apply (Nat.lt_succ_r m N). assumption. intro. rewrite e. assumption. intro. right. exists (S N). apply toCle. apply le_n. assumption. intro. right. case s. intro j. intros. exists j. apply toCle. apply Nat.le_trans with (m := N). apply Cle_to. assumption. apply Nat.le_succ_diag_r. assumption. Qed.
imports: CoRN.reals.Bridges_LUB