diff --git a/probability/fsdist.v b/probability/fsdist.v
index ac89880a..cc758b70 100644
--- a/probability/fsdist.v
+++ b/probability/fsdist.v
@@ -671,14 +671,6 @@ Implicit Types (p : prob) (a b c : {dist A}).
 Local Open Scope reals_ext_scope.
 Local Open Scope convex_scope.
 
-(* looks like to be only used in monae/proba_monad_model.v;
-   should either be removed (preferably also changing the ProbaMonad interface),
-   or have the name changed to fsdist_convA0 *)
-Definition fsdist_convA (p q r s : prob) (mx my mz : {dist A}) :
-  p = r * s :> R /\ s.~ = p.~ * q.~ ->
-  mx <| p |> (my <| q |> mz) = (mx <| r |> my) <| s |> mz.
-Proof. by case=> ? ? ; exact: convA0. Qed.
-
 Lemma finsupp_conv_subr a b p :
   p != 0%:pr -> finsupp a `<=` finsupp (a <|p|> b).
 Proof.