proposition: Lemma beta02_lim : forall x t, is_derive_n (fun u => beta x u) 2 t (beta02 x t).
proof: Proof. intros x t. unfold beta. auto_derive_2. split. apply Iu1. repeat split. apply filter_forall. apply Cu1. apply filter_forall. apply Cu1. repeat split ; apply Du1. unfold beta02, Rminus, Rdiv. now field. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)