diff options
| author | Cyril Cohen | 2017-12-14 19:10:41 +0100 |
|---|---|---|
| committer | GitHub | 2017-12-14 19:10:41 +0100 |
| commit | f4b724043fc6efc968430227c0f953c17966f445 (patch) | |
| tree | 4525c1798cd454a80c8c8a66ee2d5b33999bd2c4 /mathcomp | |
| parent | 7ed910eed93cbd5523a731998b1d2c87db712b94 (diff) | |
| parent | f0c46d647c7f5c7dc88cb2b06d20ea92ae2f9da1 (diff) | |
Merge pull request #167 from hivert/PR2
Resubmitted lemma reshape_index_leq for discussion
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index fa3bf25..5574892 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2623,6 +2623,19 @@ elim: ss => //= s ss IHss in i *; rewrite subn_eq0 nth_cat. by have [//|le_s_i] := ltnP; rewrite subnDA subSn /=. Qed. +Lemma reshape_leq sh i1 i2 + (r1 := reshape_index sh i1) (c1 := reshape_offset sh i1) + (r2 := reshape_index sh i2) (c2 := reshape_offset sh i2) : + (i1 <= i2) = ((r1 < r2) || ((r1 == r2) && (c1 <= c2))). +Proof. +rewrite {}/r1 {}/c1 {}/r2 {}/c2 /reshape_offset /reshape_index. +elim: sh => [|s0 s IHs] /= in i1 i2 *; rewrite ?subn0 ?subn_eq0 //. +have [[] i1s0 [] i2s0] := (ltnP i1 s0, ltnP i2 s0); first by rewrite !subn0. +- by apply: leq_trans i2s0; apply/ltnW. +- by apply/negP => /(leq_trans i1s0); rewrite leqNgt i2s0. +by rewrite !subSn // !eqSS !ltnS !subnDA -IHs leq_subLR subnKC. +Qed. + End Flatten. Prenex Implicits flatten shape reshape. |