proposition: Lemma is_derive_0_is_cst (f : R -> R) x y : (forall x, is_derive x (1 : R) f 0) -> f x = f y.
proof: Proof. move=> Hd. wlog xLy : x y / x <= y by move=> H; case: (leP x y) => [/H |/ltW /H]. rewrite -(subKr (f y) (f x)). have [| _ _] := MVT_segment xLy; last by rewrite mul0r => ->; rewrite subr0. apply/continuous_subspaceT=> r. exact/differentiable_continuous/derivable1_diffP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)