diff options
| author | Cyril Cohen | 2018-02-06 19:36:53 +0100 |
|---|---|---|
| committer | GitHub | 2018-02-06 19:36:53 +0100 |
| commit | d6bc72cd477ed6fe8b95782b26a2e0fc92711395 (patch) | |
| tree | 6996e39182b97573b1cdecaeb7c8c8a3f58c1e77 /mathcomp/algebra/ssrint.v | |
| parent | 11e539dae1bfe8bc67fc7bd1eb65ee3b4c29f813 (diff) | |
| parent | f3ce9ace4b55654d6240db9eb41a6de3c488f0d9 (diff) | |
Merge pull request #164 from CohenCyril/linting
linting of the whole library
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index eb66940..e6c4ca6 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -120,7 +120,7 @@ Lemma int_rect (P : int -> Type) : -> (forall n : nat, P (- n) -> P (- (n.+1))) -> forall n : int, P n. Proof. -by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp]. +by move=> P0 hPp hPn []; elim=> [|n ihn]//; do ?[apply: hPn | apply: hPp]. Qed. Definition int_rec := int_rect. @@ -210,7 +210,7 @@ Lemma int_rect (P : int -> Type) : -> (forall n : nat, P (- (n%:Z)) -> P (- (n.+1%N%:Z))) -> forall n : int, P n. Proof. -by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp]. +by move=> P0 hPp hPn []; elim=> [|n ihn]//; do ?[apply: hPn | apply: hPp]. Qed. Definition int_rec := int_rect. @@ -546,7 +546,7 @@ case: (leqP m n)=> hmn; rewrite /intmul //=. rewrite -{2}[n](@subnKC m)// mulrnDr opprD addrA subrr sub0r. by case hdmn: (_ - _)%N=> [|dmn] /=; first by rewrite mulr0n oppr0. have hnm := ltnW hmn. -rewrite -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r. +rewrite -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r. by rewrite subzn. Qed. |