proposition: Lemma beta01_lim : forall x t, is_derive (fun u => beta x u) t (beta01 x t).
proof: Proof. intros x t. unfold beta. auto_derive. split. apply Iu1. repeat split. apply filter_forall. apply Cu1. apply filter_forall. apply Cu1. unfold beta01, Rminus, Rdiv. now field. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)