From 6c4382c69e72b81fb7e81b0b753e5d3c83b1064a Mon Sep 17 00:00:00 2001
From: Sora Chen
Date: Wed, 8 May 2019 05:37:41 +0800
Subject: suppress use of `Arith` hints

---
 mathcomp/algebra/ssrint.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/ssrint.v')

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 1b1eb77..3c4c002 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1553,7 +1553,7 @@ Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed.
 Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed.
 
 Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|.
-Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed.
+Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2] //=; rewrite ?mulnS mulnC. Qed.
 
 Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n.
 Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed.
-- 
cgit v1.2.3