proposition: Lemma 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) -> {m : nat | {Hm : m <= n | P m Hm}} or (forall i H, Q i H).
proof: Proof. intro n; induction n as [| n Hrecn]. intros P Q HP HQ H. elim (H _ (le_n 0)); intro H0. left; exists 0; exists (le_n 0); assumption. right; intros i H1. apply HQ with (H := le_n 0); auto with arith. intros P Q H H0 H1. elim (H1 _ (le_n (S n))); intro H2. left; exists (S n); exists (le_n (S n)); assumption. 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 *. cut ({m : nat | {Hm : m <= n | P' m Hm}} or (forall (i : nat) (H : i <= n), Q' i H)). intro H3; elim H3; intro H4. left. elim H4; intros m Hm; elim Hm; clear H4 Hm; intros Hm Hm'. exists m. unfold P' in Hm'. exists (le_S _ _ Hm). eapply H with (i := m); [ lia | apply Hm' ]. right. intros i H5. unfold Q' in H4. elim (le_lt_eq_dec _ _ H5); intro H6. cut (i <= n); [ intro | auto with arith ]. eapply H0 with (i := i); [ auto with arith | apply (H4 i H7) ]. eapply H0 with (i := S n); [ auto with arith | apply H2 ]. apply Hrecn. intro i; intros j H3 H4 H5 H6. unfold P' in |- *. exact (H _ _ H3 _ _ H6). intro i; intros j H3 H4 H5 H6. unfold Q' in |- *. exact (H0 _ _ H3 _ _ H6). intros i H3. 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)