proposition: Lemma trick' : forall (n : nat) (r g : nat -> OF), (forall m : nat, m <= n -> g m[<][0]) -> (forall m : nat, m <= n -> g m[<]r m) -> forall m : nat, m <= n -> Hum g n[<]r m.
proof: Proof. intros n r g H H0 m H1. induction n as [| n Hrecn]. simpl in |- *. rewrite <- (proj1 (Nat.le_0_r m) H1). apply H0. apply H1. simpl in |- *. case (le_lt_eq_dec m (S n)). assumption. intro. cut (m <= n). intro. astepr (([0]:OF)[+]r m). apply plus_resp_less_both. apply H. apply le_n. apply Hrecn. intros. apply H. apply Nat.le_trans with (m := n). assumption. apply Nat.le_succ_diag_r. intros. apply H0. apply Nat.le_trans with (m := n). assumption. apply Nat.le_succ_diag_r. assumption. apply Nat.lt_succ_r. assumption. intro H2. rewrite H2. astepr (r (S n)[+]([0]:OF)). apply plus_resp_less_both. apply H0. apply le_n. apply bound_tk2. intros. apply H. apply Nat.le_trans with (m := n). assumption. apply Nat.le_succ_diag_r. Qed.
imports: CoRN.reals.Bridges_LUB