proposition: Lemma eta_exists : {eta : IR | [0] [<] eta | {b_0' : CC | AbsCC (b_0'[-]b_0) [<=] eta | b_0' [#] [0] and AbsCC b_0'[+]Three[*]eta [<] c}}.
proof: Proof. exists eta_0. exact eta_0_pos. generalize (b_0'_exists eta_0 eta_0_pos). intro H. elim H. intros b_0' H0 H1. exists b_0'. assumption. split. assumption. apply leEq_less_trans with ((AbsCC b_0[+]c) [/]TwoNZ). 2: apply Average_less_Greatest; auto. apply shift_plus_leEq. apply leEq_wdl with (AbsCC (b_0'[-]b_0[+]b_0)). 2: apply AbsCC_wd; rational. apply leEq_transitive with (AbsCC (b_0'[-]b_0) [+]AbsCC b_0). apply triangle. apply leEq_transitive with (eta_0[+]AbsCC b_0). apply plus_resp_leEq; auto. apply eq_imp_leEq. unfold eta_0 in |- *; rational. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma