proposition: Lemma C1_continuation_derive_eq : forall a b d x, a <= x <= b -> C1_continuation_derive d a b x = d x.
proof: Proof. intros a b d x Hx. unfold C1_continuation_derive. destruct (Rlt_dec x a). apply False_ind; apply (Rlt_not_le _ _ r), (proj1 Hx). destruct (Rle_dec x b). reflexivity. apply False_ind, n0, (proj2 Hx). Qed.
imports: Reals Lra Rfunctions