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

refactor(library/algebra/ordered_group): use rewrite tactic at ordered_group

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-08 17:35:28 -08:00
parent f9ff4ee6bd
commit c7ee831c69
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/algebra/ordered_group.lean
View file

@ -141,7 +141,7 @@ section
have Hbz : b = 0, from le.antisymm Hb' Hb, have Hbz : b = 0, from le.antisymm Hb' Hb,
and.intro Haz Hbz) and.intro Haz Hbz)
(assume Hab : a = 0 ∧ b = 0, (assume Hab : a = 0 ∧ b = 0,
(and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_zero 0)) and.elim Hab (λ Ha Hb, by rewrite [Ha, Hb, add_zero]))
theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c := theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c :=
!zero_add ▸ add_le_add Ha Hbc !zero_add ▸ add_le_add Ha Hbc
@ -200,8 +200,8 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
(add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b)) (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c := theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _, have H' [visible] : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H' by rewrite *neg_add_cancel_left at H'; exact H'
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible] definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A := [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=