proposition: Lemma om_fun_2a : forall n m f g Hfg (x : F), (forall i Hi, f i Hi [<] x) -> (forall i Hi, g i Hi [<] x) -> forall i Hi, om_fun n m f g Hfg i Hi [<] x.
proof: Proof. intro n. induction n as [| n Hrecn]. simpl in |- *; auto. intro m; induction m as [| m Hrecm]. simpl in |- *; auto. intros. simpl in |- *; elim ap_imp_less; simpl in |- *; intro; elim le_lt_eq_dec; simpl in |- *; intro; auto. set (h := fun (i : nat) (Hi : i < m) => 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 *. set (Hh := fun i Hi => X0 i (Nat.lt_lt_succ_r _ _ Hi)) in *. exact (Hrecm f h Hfh x X Hh i (om_fun_lt _ _ a0)). Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)