proposition: Lemma Continuous_imp_pos : forall a b c (Hac : a [<=] c), a [<=] b -> b [<] c -> forall F, Continuous_I Hac F -> (forall t, a [<=] t -> t [<=] b -> forall Ht, [0] [<] F t Ht) -> (forall t, b [<] t -> t [<=] c -> forall Ht, [0] [<] F t Ht) -> forall t, a [<=] t -> t [<=] c -> forall Ht, [0] [<] F t Ht.
proof: Proof. intros a b c Hac H H0 F H1 H2 H3 t H4 H5 Ht. elim H1; intros H6 H7; clear H1. cut (Compact Hac b); [ intro H1 | split; auto ]. 2: apply less_leEq; auto. set (e := F b (H6 _ H1) [/]TwoNZ) in *. cut ([0] [<] e); intros. 2: unfold e in |- *; apply pos_div_two; apply H2; auto. 2: apply leEq_reflexive. elim H7 with e; auto. intros d H9 H10. cut (b[-]d [<] b). 2: apply shift_minus_less; apply shift_less_plus'. 2: astepl ZeroR; auto. intro H11. elim (less_cotransitive_unfolded _ _ _ H11 t); intro. clear H11. elim (less_cotransitive_unfolded _ _ _ H9 (t[-]b)); intro. apply H3. astepl ([0][+]b); apply shift_plus_less; auto. auto. apply cont_no_sign_change_pos with (Hab := Hac) (e := e) (Hx := H6 _ H1); auto. split; auto. apply H10; auto. split; auto. apply AbsSmall_imp_AbsIR. apply AbsIR_eq_AbsSmall. rstepr ( [--] (t[-]b)); apply inv_resp_leEq. apply less_leEq; auto. apply less_leEq; apply shift_minus_less; apply shift_less_plus'; auto. unfold e in |- *. eapply less_leEq_trans. apply pos_div_two'. apply H2; auto. apply leEq_reflexive. apply leEq_AbsIR. unfold e in |- *. apply pos_div_two'. apply H2; auto. apply leEq_reflexive. apply H2; auto. apply less_leEq; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3