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/attic/fib.v | |
| parent | 11e539dae1bfe8bc67fc7bd1eb65ee3b4c29f813 (diff) | |
| parent | f3ce9ace4b55654d6240db9eb41a6de3c488f0d9 (diff) | |
Merge pull request #164 from CohenCyril/linting
linting of the whole library
Diffstat (limited to 'mathcomp/attic/fib.v')
| -rw-r--r-- | mathcomp/attic/fib.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v index fefa0d2..a75a226 100644 --- a/mathcomp/attic/fib.v +++ b/mathcomp/attic/fib.v @@ -59,15 +59,15 @@ Proof. by []. Qed. Lemma lin_fib_alt : forall n a b, lin_fib a b n.+2 = lin_fib a b n.+1 + lin_fib a b n. Proof. -case=>//; elim => [//|n IHn] a b. +case=> //; elim=> [//|n IHn] a b. by rewrite lin_fibSS (IHn b (b + a)) lin_fibE. Qed. Lemma fib_is_linear : fib =1 lin_fib 0 1. Proof. -move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn]. +move=> n; elim: n {-2}n (leqnn n)=> [n|n IHn]. by rewrite leqn0; move/eqP=>->. -case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite fibSS lin_fib_alt. +case=> //; case=> // n0; rewrite ltnS=> ltn0n; rewrite fibSS lin_fib_alt. by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). Qed. @@ -132,7 +132,7 @@ case: m=> [|[|m]] Hm. - by rewrite eq_sym fib_eq1 orbF [1==_]eq_sym; case: eqP. have: 1 < m.+2 < n by []. move/fib_smonotone; rewrite ltn_neqAle; case/andP; move/negPf=> -> _. -case: n Hm=> [|[|n]] //;rewrite ltn_neqAle; case/andP; move/negPf=> ->. +case: n Hm=> [|[|n]] //; rewrite ltn_neqAle; case/andP; move/negPf=> ->. by rewrite andbF. Qed. @@ -154,7 +154,7 @@ case/orP: (Hf _ (dvdn_fib _ _ (dvdn_mulr d (dvdnn k)))). rewrite fib_eq; case/or3P; first by move/eqP<-; rewrite eqxx orbT. by case/andP=>->. by rewrite Hk; case: (d)=> [|[|[|]]]. -rewrite fib_eq; case/or3P; last by case/andP;move/eqP->; case: (d)=> [|[|]]. +rewrite fib_eq; case/or3P; last by case/andP; move/eqP->; case: (d)=> [|[|]]. rewrite -{1}[k]muln1; rewrite eqn_mul2l; case/orP; move/eqP=> HH. by move: Pp; rewrite Hp HH. by rewrite -HH eqxx. @@ -216,9 +216,9 @@ Proof. by []. Qed. Lemma lucas_is_linear : lucas =1 lin_fib 2 1. Proof. -move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn]. +move=> n; elim: n {-2}n (leqnn n)=> [n|n IHn]. by rewrite leqn0; move/eqP=>->. -case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt. +case=> //; case=> // n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt. by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). Qed. @@ -329,7 +329,7 @@ Local Notation "''M{' l } " := (seq2matrix _ _ l). Lemma matrix_fib : forall n, 'M{[:: [::(fib n.+2)%:R; (fib n.+1)%:R]; - [::(fib n.+1)%:R; (fib n)%:R]]} = + [::(fib n.+1)%:R; (fib n)%:R]]} = ('M{[:: [:: 1; 1]; [:: 1; 0]]})^+n.+1 :> 'M[R]_(2,2). Proof. |