diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b8315e845..b27e544cf 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -25,6 +25,7 @@
     `completed_caratheodory_measurable`
 - in `ftc.v`:
   + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`)
+  + lemma `FTC1Ny`
 
 ### Changed
 
diff --git a/theories/ftc.v b/theories/ftc.v
index 0ffe796be..ab9f19614 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -205,6 +205,15 @@ apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
 by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr.
 Qed.
 
+Corollary FTC1Ny f : mu.-integrable setT (EFin \o f) ->
+  let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
+  {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}.
+Proof.
+move=> intf F; have := FTC1 -oo%O intf.
+apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
+by move=> r /=; apply; rewrite ltNyr.
+Qed.
+
 Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   forall x, a < BRight x -> {for x, continuous f} ->