proposition: Lemma om_fun_3a : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g -> forall i Hi, {j : nat | {Hj : j < m + n | f i Hi [=] om_fun n m f g Hfg j Hj}}.
proof: Proof. intro n. induction n as [| n Hrecn]. simpl in |- *; intros. exfalso; inversion Hi. intro m; induction m as [| m Hrecm]. simpl in |- *; intros. exists i. exists Hi. algebra. intros. simpl in |- *; elim ap_imp_less; simpl in |- *; intro. set (h := fun i Hi => g i (Nat.lt_lt_succ_r _ _ Hi)) in *. set (Hfh := fun i j Hi Hj => Hfg i j Hi (Nat.lt_lt_succ_r _ _ Hj)) in *. assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto. elim (Hrecm f h Hfh H Hh i Hi); intros j Hj. elim Hj; clear Hj; intros Hj Hj'. exists j; exists (Nat.lt_lt_succ_r _ _ Hj). elim le_lt_eq_dec; simpl in |- *; intro. astepl (om_fun _ _ f h Hfh _ Hj). refine (om_fun_1 _ _ f h Hfh H Hh j j _ Hj (om_fun_lt _ _ a0)). auto. exfalso; auto with zarith. elim (le_lt_eq_dec _ _ Hi); intro. set (h := fun i Hi => f i (Nat.lt_lt_succ_r _ _ Hi)) in *. set (Hfh := fun i j Hi Hj => Hfg i j (Nat.lt_lt_succ_r _ _ Hi) Hj) in *. assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto. elim (Hrecn _ h g Hfh Hh H0 i (om_fun_lt _ _ a)); intros j Hj. elim Hj; clear Hj; intros Hj Hj'. cut (j < S (m + S n)). intro. 2: auto with zarith. exists j; exists H1. elim le_lt_eq_dec; simpl in |- *; intro. eapply eq_transitive_unfolded. eapply eq_transitive_unfolded. 2: apply Hj'. unfold h in |- *; apply H; auto. apply om_fun_1; auto. exfalso; auto with zarith. exists (m + S n). exists (Nat.lt_succ_diag_r (m + S n)). elim le_lt_eq_dec; simpl in |- *; intro. exfalso; auto with zarith. apply H. inversion b0. auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)