proposition: Lemma Kneser_1 : forall a_0 eta eps : IR, [0] [<] eta -> [0] [<] eps -> a_0[+]Three[*]eta [<] c -> Two[*] (Three[^]n[+][1]) [*]eps [<=] eta -> q[*]a_0[+]Three[^]n[*]eps[+]eps[+]eta [<] q[*]c.
proof: Proof. intros. cut ([1] [/]TwoNZ[*] (Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta) [<=] q[*] (Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta)). intro Hm. apply leEq_less_trans with (q[*] (a_0[+]Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta)). rstepr (q[*]a_0[+]q[*] (Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta)). rstepl (q[*]a_0[+][1] [/]TwoNZ[*] (Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta)). apply plus_resp_leEq_lft; auto. apply mult_resp_less_lft. apply leEq_less_trans with (a_0[+]Three[*]eta); auto. rstepl (a_0[+] (Two[*]Three[^]n[*]eps[+]Two[*]eps[+]Two[*]eta)). apply plus_resp_leEq_lft. rstepl (Two[*] (Three[^]n[+][1]) [*]eps[+]Two[*]eta). rstepr (eta[+]Two[*]eta). apply plus_resp_leEq; auto. apply less_leEq_trans with (Half:IR). apply pos_half. exact Kneser_1'. apply mult_resp_leEq_rht. exact Kneser_1'. apply less_leEq. apply less_leEq_trans with ([0][+]Two[*]eta). rstepr (Two[*]eta). apply mult_resp_pos; auto. apply pos_two. apply less_leEq. apply plus_resp_less_rht. apply less_transitive_unfolded with ([0][+]Two[*]eps). rstepr (Two[*]eps). apply mult_resp_pos; auto. apply pos_two. apply plus_resp_less_rht. repeat apply mult_resp_pos; auto. apply pos_two. apply nexp_resp_pos; apply pos_three. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma