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