diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/attic/multinom.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/attic/multinom.v')
| -rw-r--r-- | mathcomp/attic/multinom.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/attic/multinom.v b/mathcomp/attic/multinom.v index 175da6c..96a8071 100644 --- a/mathcomp/attic/multinom.v +++ b/mathcomp/attic/multinom.v @@ -107,7 +107,7 @@ Definition multi_var n (i : 'I_n) := cast_multi (subnK (valP i)) 'X. Notation "'X_ i" := (multi_var i). Lemma inject_is_rmorphism : forall m n, rmorphism (@inject n m). -Proof. +Proof. elim=> // m ihm n /=; have ->: inject m = RMorphism (ihm n) by []. by rewrite -/(_ \o _); apply: rmorphismP. Qed. @@ -132,14 +132,14 @@ Lemma cast_multi_inj n i i' n' (m1 m2 : multi n) cast_multi p1 m1 == cast_multi p2 m2 = (m1 == m2). Proof. have := p2; rewrite -{1}[n']p1; move/eqP; rewrite eqn_add2r. -move=> /eqP /= Eii; move:p2; rewrite Eii=> p2 {Eii}. +move=> /eqP /= Eii; move: p2; rewrite Eii=> p2 {Eii}. have <-: p1 = p2; first exact: nat_irrelevance. apply/idP/idP; last by move/eqP->. -move => Hm {p2}. +move=> Hm {p2}. have : inject i m1 = inject i m2; last first. by move/eqP; rewrite (inj_eq (@inject_inj _ _)). -move: Hm; move:(p1); rewrite -p1 => p2. -rewrite (_ : p2 = erefl (i+n)%N); last exact: nat_irrelevance. +move: Hm; move: (p1); rewrite -p1 => p2. +rewrite (_ : p2 = erefl (i+n)%N); last exact: nat_irrelevance. by move/eqP. Qed. @@ -195,8 +195,8 @@ Lemma interp_cast_multi n n' m (nltn' : n <= n') : Proof. move=> dmltn; have dmltn' := (leq_trans dmltn nltn'). elim: m nltn' dmltn dmltn'. -+ move=> a /= nltn' dmltn dmltn'. - apply/eqP; rewrite /multiC. ++ move=> a /= nltn' dmltn dmltn'. + apply/eqP; rewrite /multiC. by rewrite cast_multi_add /= cast_multi_inj. + move=> N /= nltn' dmltn dmltn'. move: (refl_equal (_ N < n')) (refl_equal (_ N < n)). |