proposition: Lemma pderivable_restrict_right : pderivable f (fun x => a <= x < b) -> forall a' b', a <= a' -> b' < b -> a' < b' -> pderivable f (fun x => a' <= x <= b').
proof: Proof. move=> H a' b' aa' bb' a'b' z [z0 z1]; apply H; lra. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext