proposition: Lemma alpha_02_lim : forall x t, is_derive_n (fun u => alpha x u) 2 t (alpha02 x t).
proof: Proof. intros x t. unfold alpha. auto_derive_2. repeat split ; apply Du0. repeat split ; apply D2u0. unfold alpha02, Derive_n, Rminus, Rdiv. ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)