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

feat(algebra/ordered_field): add missing theorems about division

Browse source
This commit is contained in:
Rob Lewis 2016-04-18 13:45:37 -04:00 committed by Leonardo de Moura
parent 3482e1eab9
commit 89de67f4c3
1 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
library/algebra/ordered_field.lean
View file

@ -371,6 +371,21 @@ section linear_ordered_field
apply (not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc')
end
theorem mul_div_self_add_lt {b c d : A} (Hb : b > 0) (Hc : c > 0) (Hd : d > 0) : c * (b / (c + d)) < b :=
begin
rewrite -mul_div_assoc,
apply div_lt_of_mul_lt_of_pos,
apply add_pos,
repeat assumption,
rewrite mul.comm,
apply mul_lt_mul_of_pos_left,
apply lt_add_of_pos_right,
repeat assumption
end
theorem mul_div_add_self_lt {b c d : A} (Hb : b > 0) (Hc : c > 0) (Hd : d > 0) : d * (b / (c + d)) < b :=
by rewrite add.comm; apply mul_div_self_add_lt; repeat assumption
end linear_ordered_field
structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,
@ -571,6 +586,6 @@ section discrete_linear_ordered_field
div_nonneg_of_nonneg_of_pos Ha Hgt
else
have b = 0, from eq_of_le_of_ge (le_of_not_gt Hgt) Hb,
by+ rewrite [this, div_zero]; apply le.refl
by rewrite [this, div_zero]; apply le.refl
end discrete_linear_ordered_field