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

refactor(ordered_group): replace 'match' with 'obtain'

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-06 10:34:43 -07:00
parent 613281d622
commit 64cc710ff7
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/algebra/ordered_group.lean
View file

@ -152,9 +152,8 @@ section
have Hbz : b = 0, from le.antisymm Hb' Hb,
and.intro Haz Hbz)
(assume Hab : a = 0 ∧ b = 0,
match Hab with
| and.intro Ha' Hb' := by rewrite [Ha', Hb', add_zero]
end)
obtain Ha' Hb', from Hab,
by rewrite [Ha', Hb', add_zero])
theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c :=
!zero_add ▸ add_le_add Ha Hbc