proposition: Lemma Cu1 : forall x, continuity_pt (fun u => u1 u) x.
proof: Proof. intros x. destruct (Du1 x) as (l,Hl). apply derivable_continuous_pt. unfold derivable_pt, derivable_pt_abs. exists l. now apply is_derive_Reals. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)