Merge pull request #40 from coq-community/mc_1223

Adapt to math-comp/math-comp#1223
coq-community · Jun 29, 2024 · 4bc2960 · 4bc2960
2 parents 080d923 + 5487c74
commit 4bc2960
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.