From 5487c744c2286196575c06a54e6ed5bd3bf28a58 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 29 Jun 2024 15:47:15 +0200
Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1223

---
 theories/core/completeness.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/core/completeness.v b/theories/core/completeness.v
index 3cabc9b..957f9eb 100644
--- a/theories/core/completeness.v
+++ b/theories/core/completeness.v
@@ -94,7 +94,7 @@ Proof.
       suff E: input=output :>G by congruence.
       apply/(card_le1_eqP (A := predT)) => //.
       apply iso_v, card_bij in L. rewrite !card_sum !card_unit addnC in L.
-        by injection L=>->.
+      by case: L; rewrite ?add0n => ->.
     * have E: forall y, L (inr tt) <> L (inl y) by intros y H; generalize (bij_injective (f:=L) H). 
       case_eq (L (inr tt)); case.
        generalize (E input). simpl in *. congruence.