michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/algebra/ordered_ring): use 'note'

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-15 09:33:57 -08:00
parent ec5990f4de
commit 42eda36225
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/ordered_ring.lean
View file

@ -440,8 +440,8 @@ section
begin
apply le_of_not_gt,
intro Hab,
let Hposa := lt_of_le_of_lt Hb Hab,
let H' := calc
note Hposa := lt_of_le_of_lt Hb Hab,
note H' := calc
b * b ≤ a * b : mul_le_mul_of_nonneg_right (le_of_lt Hab) Hb
... < a * a : mul_lt_mul_of_pos_left Hab Hposa,
apply (not_le_of_gt H') H