proposition: Lemma om_fun_4c : forall n m f g Hfg (P : F -> CProp), pred_wd F P -> nat_less_n_fun f -> nat_less_n_fun g -> {i : nat | {Hi : i < n | P (f i Hi)}} or {j : nat | {Hj : j < m | P (g j Hj)}} -> {k : nat | {Hk : k < m + n | P (om_fun n m f g Hfg k Hk)}}.
proof: Proof. intros n m f g Hfg P HP Hf Hg H. elim H; intro H'; elim H'; intros i Hi; elim Hi; clear H H' Hi; intros Hi Hi'. elim (om_fun_3a _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj. intros Hj Hj'. exists j; exists Hj; apply HP with (x := f i Hi); auto. elim (om_fun_3b _ _ _ _ Hfg Hf Hg i Hi). intros j Hj. elim Hj; clear Hj. intros Hj Hj'. exists j; exists Hj; apply HP with (x := g i Hi); auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)