diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/ssreflect/path.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 7d1f0e9..0965b14 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -865,7 +865,7 @@ apply: ihss. rewrite (perm_mem perm_s2) mem_iota => /andP [] _ hy'. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota => /andP []. by rewrite -cat_cons size_cat addnC => /(leq_trans hy'). -- rewrite /= perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite /= perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. @@ -880,7 +880,7 @@ apply: ihss => /=. apply/allP => m'; rewrite (perm_mem perm_s2) mem_iota => /andP [_ hm']. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota -cat_cons size_cat. by rewrite addnC => /andP [] /(leq_trans hm'). -- rewrite perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. |