diff --git a/README.md b/README.md
index d7d8a07..4cdfa8b 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@ principle.
 
 This branch requires the [mathcomp-analysis
 library](https://github.com/math-comp/analysis) and its dependencies and the
-[ssring.v](https://github.com/jasmin-lang/jasmin/blob/f1f8b193591d369296d5661f0ae8a09f3b6eaa9b/proofs/3rdparty/ssrring.v)
+[ssring.v](https://raw.githubusercontent.com/jasmin-lang/jasmin/f1f8b193591d369296d5661f0ae8a09f3b6eaa9b/proofs/3rdparty/ssrring.v)
 file from [jasmin](https://github.com/jasmin-lang/jasmin).
 
 It is organised as follows:
diff --git a/pendulum.v b/pendulum.v
index f30a1c3..7812b36 100644
--- a/pendulum.v
+++ b/pendulum.v
@@ -132,7 +132,7 @@ by rewrite (splitr e%:num) ltr_add //; [apply/p2e1_sp2he|apply/p3e2_sp3he];
   apply: ball_ler (pme12_q _ _); rewrite ler_minl lerr // orbC.
 Qed.
 
-Lemma preimV_lek0_closed : closed (V @^-1` (<= k0)).
+Lemma preimV_lek0_closed : closed (V @^-1` (<= k0 : _ -> _)).
 Proof.
 by apply: closed_comp; [move=> ??; apply: V_continuous|apply: closed_le].
 Qed.