proposition: Lemma prolongement_C1_C1 : forall (f d : R -> R) (a b : R), a <= b -> (forall c, a <= c <= b -> derivable_pt_abs f c (d c)) -> (forall c, a <= c <= b -> continuity_pt d c) -> {g : C1_fun | (forall c : R, a <= c <= b -> f c = g c) /\ (forall c : R, a <= c <= b -> d c = derive g (diff0 g) c)}.
proof: Proof. intros f d a b Hab Hder Hcont. pose proof (prolongement_C1_derivable f d a b Hab Hder) as [diff0 Heq]. pose proof (C1_continuation_derive_continuous d a b Hab Hcont) as cont. assert(c1 : continuity (derive (C1_continuation f a b d) diff0)). intros x eps Heps. destruct (cont x eps Heps) as [alpha [Halpha1 Halpha2]]. exists alpha. split. assumption. intros. do 2 rewrite Heq; intuition. exists (mkC1 c1). split. intros x Hx. rewrite <- (C1_continuation_eq f a b d x Hx); reflexivity. intros x Hx. rewrite <- (C1_continuation_derive_eq a b d x Hx), Heq; reflexivity. Qed.
imports: Reals Lra Rfunctions