proposition: Lemma om_fun_2 : forall n m f g Hfg, nat_less_n_fun f -> nat_less_n_fun g -> (forall i i' Hi Hi', i < i' -> f i Hi [<] f i' Hi') -> (forall i i' Hi Hi', i < i' -> g i Hi [<] g i' Hi') -> forall i i' Hi Hi', i < i' -> om_fun n m f g Hfg i Hi [<] om_fun n m f g Hfg i' Hi'.
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; repeat (elim le_lt_eq_dec; simpl in |- *; intro); try (exfalso; auto with zarith; fail). 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. set (inch := fun i i' Hi Hi' Hii' => X0 i i' (Nat.lt_lt_succ_r _ _ Hi) (Nat.lt_lt_succ_r _ _ Hi') Hii') in *. exact (Hrecm f h Hfh H Hh X inch i i' (om_fun_lt _ _ a0) (om_fun_lt _ _ a1) H1). 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. refine (om_fun_2a _ _ f h Hfh (g m (Nat.lt_succ_diag_r m)) _ _ i (om_fun_lt _ _ a0)). intros j Hj. elim (le_lt_eq_dec _ _ Hj); intro. apply less_transitive_unfolded with (f n (Nat.lt_succ_diag_r n)); auto with arith. apply less_wdl with (f n (Nat.lt_succ_diag_r n)); auto. apply H; auto. inversion b0. auto. unfold h in |- *; auto. apply Hrecn; auto. red in |- *; auto. apply om_fun_2a; auto. intros j Hj. elim (le_lt_eq_dec _ _ Hj); intro. apply less_transitive_unfolded with (g m (Nat.lt_succ_diag_r m)); auto with arith. apply less_wdl with (g m (Nat.lt_succ_diag_r m)); auto. apply H0; auto. inversion b1. auto. Qed.
imports: CoRN.algebra.COrdCauchy Coq(Lia)