We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b522ecf commit e3de89dCopy full SHA for e3de89d
1 file changed
classical/unstable.v
@@ -65,7 +65,7 @@ Proof.
65
apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
66
case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
67
by rewrite addrCA addrK.
68
-by rewrite addrC subrKA.
+by rewrite (addrC (x + y)) subrKA.
69
Qed.
70
71
Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.
0 commit comments