proposition: Lemma om_fun_1 : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g -> nat_less_n_fun (om_fun n m f g Hfg).
proof: Proof. intro n. induction n as [| n Hrecn]. red in |- *; simpl in |- *; auto. intro m; induction m as [| m Hrecm]. red in |- *; simpl in |- *; auto. red in |- *; intros. simpl in |- *; elim ap_imp_less; simpl in |- *; intro; repeat (elim le_lt_eq_dec; simpl in |- *; intro); try (exfalso; auto with zarith; fail); try apply eq_reflexive_unfolded. 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 *. assert (Hh : nat_less_n_fun h). red in |- *; unfold h in |- *; auto. exact (Hrecm f h Hfh H Hh i j H1 (om_fun_lt _ _ a0) (om_fun_lt _ _ a1)). apply Hrecn; try red in |- *; auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)