diff options
| author | Cyril Cohen | 2020-09-07 15:27:49 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-07 15:27:49 +0200 |
| commit | ed040ad0db541c597a354aba126f428e42eef854 (patch) | |
| tree | 3884e9e23b799f0b970de1d5931ae944e233738b /mathcomp/algebra | |
| parent | abb204c55d28b139bb57d56fb7e3b0ae29cf5dc5 (diff) | |
compat Coq < 8.10
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 4267bbb..22f5e89 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1421,7 +1421,7 @@ Lemma trigmx_ind (P : forall m n, 'M_(m, n) -> Type) : P m n A -> P (1 + m)%N (1 + n)%N (block_mx x 0 c A)) -> forall m n A, is_trig_mx A -> P m n A. Proof. -move=> P0l P0r PS m n A; elim: A => [{}m|{}n|{}m {}n xx r c] A PA; +move=> P0l P0r PS m n A; elim: A => {m n} [m|n|m n xx r c] A PA; do ?by rewrite (flatmx0, thinmx0); by [apply: P0l|apply: P0r]. by rewrite is_trig_block_mx => // /and3P[/eqP-> _ Atrig]; apply: PS (PA _). Qed. @@ -1430,7 +1430,7 @@ Lemma trigsqmx_ind (P : forall n, 'M[V]_n -> Type) : (P 0%N 0) -> (forall n x c A, is_trig_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> forall n A, is_trig_mx A -> P n A. Proof. -move=> P0 PS n A; elim/sqmx_ind: A => [|{}n x r c] A PA. +move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. by rewrite thinmx0; apply: P0. by rewrite is_trig_block_mx => // /and3P[/eqP-> _ Atrig]; apply: PS (PA _). Qed. @@ -1452,7 +1452,7 @@ Lemma diagmx_ind (P : forall m n, 'M_(m, n) -> Type) : forall m n A, is_diag_mx A -> P m n A. Proof. move=> P0l P0r PS m n A Adiag; have Atrig := is_diag_mx_is_trig Adiag. -elim/trigmx_ind: Atrig Adiag => // {}m {}n r c {A}A _ PA. +elim/trigmx_ind: Atrig Adiag => // {m n} m n r c {A}A _ PA. rewrite is_diag_block_mx => // /and4P[_ /eqP-> _ Adiag]. exact: PS (PA _). Qed. @@ -1462,7 +1462,7 @@ Lemma diagsqmx_ind (P : forall n, 'M[V]_n -> Type) : (forall n x c A, is_diag_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) -> forall n A, is_diag_mx A -> P n A. Proof. -move=> P0 PS n A; elim/sqmx_ind: A => [|{}n x r c] A PA. +move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA. by rewrite thinmx0; apply: P0. rewrite is_diag_block_mx => // /and4P[/eqP-> /eqP-> _ Adiag]. exact: PS (PA _). |