proposition: Lemma C1_continuation_derive_continuous : forall d a b, a <= b -> (forall c, a <= c <= b -> continuity_pt d c) -> continuity (C1_continuation_derive d a b).
proof: Proof. intros d a b Hab Cd. apply (C0_sticking_two_pt _ (fct_cte (d a)) d (fct_cte (d b)) a b Hab); try (apply continuity_constant); auto; intros; unfold C1_continuation_derive; destruct (Rlt_dec x a); destruct (Rle_dec x b); auto. assert (x = a) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto). subst; trivial. pose proof Rle_antisym a x (Rnot_lt_le _ _ n) H; subst. apply (False_ind _ (n0 Hab)). apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)). apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)). apply (False_ind _ (n0 (proj2 H))). assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst. apply (False_ind _ (RIneq.Rle_not_lt _ _ Hab r)). apply False_ind; apply (RIneq.Rle_not_lt _ _ H). apply Rlt_le_trans with a; auto. assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst. trivial. Qed.
imports: Reals Lra Rfunctions