diff options
| author | Georges Gonthier | 2019-05-08 09:38:02 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-08 09:38:02 +0200 |
| commit | 51b9988f608625c60184dbe90133d64cdaa2a1f9 (patch) | |
| tree | 5315fbaebdbeca10f6a9ffba448ea424d16252b3 /mathcomp/algebra/ssrint.v | |
| parent | 02830d7cf24f9198d5e7cb81843d6ca5cb69f68a (diff) | |
| parent | 6c4382c69e72b81fb7e81b0b753e5d3c83b1064a (diff) | |
Merge pull request #344 from soraros/ssrnat-remove-arith-lemmas
remove dependence on Arith lemmas
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |