proposition: Lemma str_finite_or_elim : forall (n : nat) (P Q : forall i, i <= n -> CProp), nat_less_n_pred' P -> nat_less_n_pred' Q -> (forall i H, P i H or Q i H) -> {j : nat | {Hj : j <= n | P j Hj and (forall j' Hj', j' < j -> Q j' Hj')}} or (forall i H, Q i H).
proof: Proof. intro n; induction n as [| n Hrecn]. intros P Q H H0 H1. elim (H1 0 (le_n 0)); intro HPQ. left. exists 0; exists (le_n 0). split. apply H with (H := le_n 0); auto. intros; exfalso; inversion H2. right; intros. apply H0 with (H := le_n 0); auto with arith. intros P Q H H0 H1. set (P' := fun (i : nat) (H : i <= n) => P i (le_S _ _ H)) in *. set (Q' := fun (i : nat) (H : i <= n) => Q i (le_S _ _ H)) in *. elim (Hrecn P' Q'). intro H2. left. elim H2; intros m Hm; elim Hm; clear H2 Hm; intros Hm Hm'. exists m. unfold P' in Hm'. exists (le_S _ _ Hm). elim Hm'; clear Hm'; intros Hm' Hj. split. eapply H with (i := m); [ auto with arith | apply Hm' ]. unfold Q' in Hj; intros j' Hj' H2. cut (j' <= n); [ intro H4 | apply Nat.le_trans with m; auto with arith ]. apply H0 with (H := le_S _ _ H4); [ auto | apply Hj; assumption ]. elim (H1 (S n) (le_n (S n))); intro H1'. intro H2. left; exists (S n); exists (le_n (S n)); split. assumption. intros j' Hj' H3; unfold Q' in H1'. cut (j' <= n); [ intro H4 | auto with arith ]. unfold Q' in H2. apply H0 with (H := le_S _ _ H4); auto. intro H2. right; intros i H3. unfold Q' in H1'. elim (le_lt_eq_dec _ _ H3); intro H4. cut (i <= n); [ intro H5 | auto with arith ]. unfold Q' in H2. apply H0 with (H := le_S _ _ H5); auto. apply H0 with (H := le_n (S n)); auto. intro i; intros j H2 H3 H4 H5. unfold P' in |- *. exact (H _ _ H2 _ _ H5). intro i; intros j H2 H3 H4 H5. unfold Q' in |- *. exact (H0 _ _ H2 _ _ H5). intros i H2. unfold P', Q' in |- *. apply H1. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)