proposition: Theorem Xderive_pt_constant : forall v x, Xderive_pt (fun _ => Xreal v) x (Xmask (Xreal 0) x).
proof: Proof. intros v [|x]. exact I. unfold proj_fun. intros w. apply (derivable_pt_lim_const v). Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal