diff options
| author | Cyril Cohen | 2020-11-09 13:01:18 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-11 23:22:12 +0100 |
| commit | d84c26fa2eeeeb0029a56bac37bf1bae9f10882a (patch) | |
| tree | ab048c326c8357ca5dd59bf00db26dca64442263 /mathcomp/algebra | |
| parent | d0449f7e13f06ab7295f6919d1701e8adfa72d61 (diff) | |
Intro pattern extensions for dup, swap and apply
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index a2a2395..fc24a4b 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1678,7 +1678,7 @@ Hint Resolve real1 : core. Lemma realn n : n%:R \is @real R. Proof. by rewrite ger0_real. Qed. Lemma ler_leVge x y : x <= 0 -> y <= 0 -> (x <= y) || (y <= x). -Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) h /h; rewrite !ler_opp2. Qed. +Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) /[apply]; rewrite !ler_opp2. Qed. Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x). Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed. |