diff options
| author | Kazuhiko Sakaguchi | 2020-01-09 18:56:55 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-03-15 14:11:47 +0900 |
| commit | bdb23c100648a7e1b055d90a76eedbff9eef12f4 (patch) | |
| tree | f10ac4a79a2ec0d6e751beda2f4b59904ead58a4 /mathcomp/algebra | |
| parent | 85039b4c536a67ce936c079f519a9a8b6c33f1d6 (diff) | |
Reorder arguments of comparison predicates in order.v as they should
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index f9b4cb0..0ad7f20 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3823,17 +3823,13 @@ Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}. Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed. Lemma addr_minl : @left_distributive R R +%R min. -Proof. -by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP. -Qed. +Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed. Lemma addr_minr : @right_distributive R R +%R min. Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed. Lemma addr_maxl : @left_distributive R R +%R max. -Proof. -by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP. -Qed. +Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed. Lemma addr_maxr : @right_distributive R R +%R max. Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed. @@ -3841,7 +3837,7 @@ Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed. Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z). Proof. case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx. -by case: leP; case: leP => //; rewrite lter_pmul2l //; case: leP. +by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP. Qed. Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z). |