diff options
| author | Sora Chen | 2019-05-08 05:37:41 +0800 |
|---|---|---|
| committer | Sora Chen | 2019-05-08 05:37:41 +0800 |
| commit | 6c4382c69e72b81fb7e81b0b753e5d3c83b1064a (patch) | |
| tree | 5315fbaebdbeca10f6a9ffba448ea424d16252b3 /mathcomp/ssreflect/div.v | |
| parent | 02830d7cf24f9198d5e7cb81843d6ca5cb69f68a (diff) | |
suppress use of `Arith` hints
Diffstat (limited to 'mathcomp/ssreflect/div.v')
| -rw-r--r-- | mathcomp/ssreflect/div.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index fda425d..3cb98e8 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -538,7 +538,7 @@ Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n. Proof. by rewrite addnC gcdnDl. Qed. Lemma gcdnMl n m : gcdn n (m * n) = n. -Proof. by case: n => [|n]; rewrite gcdnE modnMl gcd0n. Qed. +Proof. by case: n => [|n]; rewrite gcdnE modnMl // muln0. Qed. Lemma gcdnMr n m : gcdn n (n * m) = n. Proof. by rewrite mulnC gcdnMl. Qed. |