proposition: Lemma cont_no_sign_change : forall e, [0] [<] e -> forall x y, I x -> I y -> forall Hx Hy, AbsIR (F x Hx[-]F y Hy) [<=] e -> e [<] AbsIR (F x Hx) -> ([0] [<] F x Hx -> [0] [<] F y Hy) and (F x Hx [<] [0] -> F y Hy [<] [0]).
proof: Proof. intros e H x y H0 H1 Hx Hy H2 H3. set (fx := F x Hx) in *. set (fy := F y Hy) in *. split; intro H4. cut (e [<] fx). intro H5. astepl (e[-]e). apply shift_minus_less; apply shift_less_plus'. apply less_leEq_trans with (fx[-]fy). apply minus_resp_less; assumption. eapply leEq_transitive; [ apply leEq_AbsIR | assumption ]. elim (less_AbsIR _ _ H H3); intro H6. assumption. exfalso. cut ([0] [<] [--]e). intro; cut (e [<] [0]). exact (less_antisymmetric_unfolded _ _ _ H). astepl ( [--][--]e); astepr ( [--]ZeroR); apply inv_resp_less; assumption. apply less_transitive_unfolded with fx; assumption. astepr (e[-]e). apply shift_less_minus. apply less_leEq_trans with (fy[-]fx). 2: eapply leEq_transitive. 3: apply H2. 2: eapply leEq_wdr; [ apply leEq_AbsIR | apply AbsIR_minus ]. unfold cg_minus in |- *; apply plus_resp_less_lft. elim (less_AbsIR _ _ H H3); intro H6. apply less_transitive_unfolded with ZeroR. apply less_transitive_unfolded with fx; assumption. astepl ( [--]ZeroR); apply inv_resp_less; assumption. astepl ( [--][--]e); apply inv_resp_less; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac