forked from leanprover-community/lean
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ordered_field.lean
441 lines (365 loc) · 16.4 KB
/
ordered_field.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
/-
Copyright (c) 2014 Robert Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Lewis, Leonardo de Moura
-/
prelude
import init.algebra.ordered_ring .field
set_option old_structure_cmd true
universe u
class linear_ordered_field (α : Type u) extends linear_ordered_ring α, field α
section linear_ordered_field
variables {α : Type u} [linear_ordered_field α]
lemma mul_zero_lt_mul_inv_of_pos {a : α} (h : 0 < a) : a * 0 < a * (1 / a) :=
calc a * 0 = 0 : by rw mul_zero
... < 1 : zero_lt_one
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne.symm (ne_of_lt h)))
... = a * (1 / a) : by rw inv_eq_one_div
lemma mul_zero_lt_mul_inv_of_neg {a : α} (h : a < 0) : a * 0 < a * (1 / a) :=
calc a * 0 = 0 : by rw mul_zero
... < 1 : zero_lt_one
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne_of_lt h))
... = a * (1 / a) : by rw inv_eq_one_div
lemma one_div_pos_of_pos {a : α} (h : 0 < a) : 0 < 1 / a :=
lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos h) (le_of_lt h)
lemma pos_of_one_div_pos {a : α} (h : 0 < 1 / a) : 0 < a :=
one_div_one_div a ▸ one_div_pos_of_pos h
lemma one_div_neg_of_neg {a : α} (h : a < 0) : 1 / a < 0 :=
gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg h) (le_of_lt h)
lemma neg_of_one_div_neg {a : α} (h : 1 / a < 0) : a < 0 :=
one_div_one_div a ▸ one_div_neg_of_neg h
lemma le_mul_of_ge_one_right {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
suffices b * 1 ≤ b * a, by rwa mul_one at this,
mul_le_mul_of_nonneg_left h hb
lemma le_mul_of_ge_one_left {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ a * b :=
by rw mul_comm; exact le_mul_of_ge_one_right hb h
lemma lt_mul_of_gt_one_right {a b : α} (hb : b > 0) (h : a > 1) : b < b * a :=
suffices b * 1 < b * a, by rwa mul_one at this,
mul_lt_mul_of_pos_left h hb
lemma one_le_div_of_le (a : α) {b : α} (hb : b > 0) (h : b ≤ a) : 1 ≤ a / b :=
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
have hbinv : 1 / b > 0, from one_div_pos_of_pos hb,
calc
1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb')
... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt hbinv)
... = a / b : eq.symm $ div_eq_mul_one_div a b
lemma le_of_one_le_div (a : α) {b : α} (hb : b > 0) (h : 1 ≤ a / b) : b ≤ a :=
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
calc
b ≤ b * (a / b) : le_mul_of_ge_one_right (le_of_lt hb) h
... = a : by rw [mul_div_cancel' _ hb']
lemma one_lt_div_of_lt (a : α) {b : α} (hb : b > 0) (h : b < a) : 1 < a / b :=
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
have hbinv : 1 / b > 0, from one_div_pos_of_pos hb, calc
1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb')
... < a * (1 / b) : mul_lt_mul_of_pos_right h hbinv
... = a / b : eq.symm $ div_eq_mul_one_div a b
lemma lt_of_one_lt_div (a : α) {b : α} (hb : b > 0) (h : 1 < a / b) : b < a :=
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
calc
b < b * (a / b) : lt_mul_of_gt_one_right hb h
... = a : by rw [mul_div_cancel' _ hb']
-- the following lemmas amount to four iffs, for <, ≤, ≥, >.
lemma mul_le_of_le_div {a b c : α} (hc : 0 < c) (h : a ≤ b / c) : a * c ≤ b :=
div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_le_mul_of_nonneg_right h (le_of_lt hc)
lemma le_div_of_mul_le {a b c : α} (hc : 0 < c) (h : a * c ≤ b) : a ≤ b / c :=
calc
a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
... ≤ b * (1 / c) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
... = b / c : eq.symm $ div_eq_mul_one_div b c
lemma mul_lt_of_lt_div {a b c : α} (hc : 0 < c) (h : a < b / c) : a * c < b :=
div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_lt_mul_of_pos_right h hc
lemma lt_div_of_mul_lt {a b c : α} (hc : 0 < c) (h : a * c < b) : a < b / c :=
calc
a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
... < b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
... = b / c : eq.symm $ div_eq_mul_one_div b c
lemma mul_le_of_div_le_of_neg {a b c : α} (hc : c < 0) (h : b / c ≤ a) : a * c ≤ b :=
div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h (le_of_lt hc)
lemma div_le_of_mul_le_of_neg {a b c : α} (hc : c < 0) (h : a * c ≤ b) : b / c ≤ a :=
calc
a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
... ≥ b * (1 / c) : mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
... = b / c : eq.symm $ div_eq_mul_one_div b c
lemma mul_lt_of_gt_div_of_neg {a b c : α} (hc : c < 0) (h : a > b / c) : a * c < b :=
div_mul_cancel b (ne_of_lt hc) ▸ mul_lt_mul_of_neg_right h hc
lemma div_lt_of_mul_lt_of_pos {a b c : α} (hc : c > 0) (h : b < a * c) : b / c < a :=
calc
a = a * c * (1 / c) : mul_mul_div a (ne_of_gt hc)
... > b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
... = b / c : eq.symm $ div_eq_mul_one_div b c
lemma div_lt_of_mul_gt_of_neg {a b c : α} (hc : c < 0) (h : a * c < b) : b / c < a :=
calc
a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
... > b * (1 / c) : mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
... = b / c : eq.symm $ div_eq_mul_one_div b c
lemma div_le_of_le_mul {a b c : α} (hb : b > 0) (h : a ≤ b * c) : a / b ≤ c :=
calc
a / b = a * (1 / b) : div_eq_mul_one_div a b
... ≤ (b * c) * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hb))
... = (b * c) / b : eq.symm $ div_eq_mul_one_div (b * c) b
... = c : by rw [mul_div_cancel_left _ (ne.symm (ne_of_lt hb))]
lemma le_mul_of_div_le {a b c : α} (hc : c > 0) (h : a / c ≤ b) : a ≤ b * c :=
calc
a = a / c * c : by rw (div_mul_cancel _ (ne.symm (ne_of_lt hc)))
... ≤ b * c : mul_le_mul_of_nonneg_right h (le_of_lt hc)
-- following these in the isabelle file, there are 8 biconditionals for the above with - signs
-- skipping for now
lemma mul_sub_mul_div_mul_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c < b / d) :
(a * d - b * c) / (c * d) < 0 :=
have h1 : a / c - b / d < 0, from calc
a / c - b / d < b / d - b / d : sub_lt_sub_right h _
... = 0 : by rw sub_self,
calc
0 > a / c - b / d : h1
... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
lemma mul_sub_mul_div_mul_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c ≤ b / d) :
(a * d - b * c) / (c * d) ≤ 0 :=
have h1 : a / c - b / d ≤ 0, from calc
a / c - b / d ≤ b / d - b / d : sub_le_sub_right h _
... = 0 : by rw sub_self,
calc
0 ≥ a / c - b / d : h1
... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
lemma div_lt_div_of_mul_sub_mul_div_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
(h : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
have (a * d - c * b) / (c * d) < 0, by rwa [mul_comm c b],
have a / c - b / d < 0, by rwa [div_sub_div _ _ hc hd],
have a / c - b / d + b / d < 0 + b / d, from add_lt_add_right this _,
by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
lemma div_le_div_of_mul_sub_mul_div_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
(h : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
have (a * d - c * b) / (c * d) ≤ 0, by rwa [mul_comm c b],
have a / c - b / d ≤ 0, by rwa [div_sub_div _ _ hc hd],
have a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right this _,
by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
lemma div_pos_of_pos_of_pos {a b : α} : 0 < a → 0 < b → 0 < a / b :=
begin
intros,
rw div_eq_mul_one_div,
apply mul_pos,
assumption,
apply one_div_pos_of_pos,
assumption
end
lemma div_nonneg_of_nonneg_of_pos {a b : α} : 0 ≤ a → 0 < b → 0 ≤ a / b :=
begin
intros, rw div_eq_mul_one_div,
apply mul_nonneg, assumption,
apply le_of_lt,
apply one_div_pos_of_pos,
assumption
end
lemma div_neg_of_neg_of_pos {a b : α} : a < 0 → 0 < b → a / b < 0 :=
begin
intros, rw div_eq_mul_one_div,
apply mul_neg_of_neg_of_pos,
assumption,
apply one_div_pos_of_pos,
assumption
end
lemma div_nonpos_of_nonpos_of_pos {a b : α} : a ≤ 0 → 0 < b → a / b ≤ 0 :=
begin
intros, rw div_eq_mul_one_div,
apply mul_nonpos_of_nonpos_of_nonneg,
assumption,
apply le_of_lt,
apply one_div_pos_of_pos,
assumption
end
lemma div_neg_of_pos_of_neg {a b : α} : 0 < a → b < 0 → a / b < 0 :=
begin
intros, rw div_eq_mul_one_div,
apply mul_neg_of_pos_of_neg,
assumption,
apply one_div_neg_of_neg,
assumption
end
lemma div_nonpos_of_nonneg_of_neg {a b : α} : 0 ≤ a → b < 0 → a / b ≤ 0 :=
begin
intros, rw div_eq_mul_one_div,
apply mul_nonpos_of_nonneg_of_nonpos,
assumption,
apply le_of_lt,
apply one_div_neg_of_neg,
assumption
end
lemma div_pos_of_neg_of_neg {a b : α} : a < 0 → b < 0 → 0 < a / b :=
begin
intros, rw div_eq_mul_one_div,
apply mul_pos_of_neg_of_neg,
assumption,
apply one_div_neg_of_neg,
assumption
end
lemma div_nonneg_of_nonpos_of_neg {a b : α} : a ≤ 0 → b < 0 → 0 ≤ a / b :=
begin
intros, rw div_eq_mul_one_div,
apply mul_nonneg_of_nonpos_of_nonpos,
assumption,
apply le_of_lt,
apply one_div_neg_of_neg,
assumption
end
lemma div_lt_div_of_lt_of_pos {a b c : α} (h : a < b) (hc : 0 < c) : a / c < b / c :=
begin
intros,
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
exact mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
end
lemma div_le_div_of_le_of_pos {a b c : α} (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c :=
begin
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
exact mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
end
lemma div_lt_div_of_lt_of_neg {a b c : α} (h : b < a) (hc : c < 0) : a / c < b / c :=
begin
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
exact mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
end
lemma div_le_div_of_le_of_neg {a b c : α} (h : b ≤ a) (hc : c < 0) : a / c ≤ b / c :=
begin
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
exact mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
end
lemma add_halves (a : α) : a / 2 + a / 2 = a :=
by { rw [div_add_div_same, ← two_mul, mul_div_cancel_left], exact two_ne_zero }
lemma sub_self_div_two (a : α) : a - a / 2 = a / 2 :=
suffices a / 2 + a / 2 - a / 2 = a / 2, by rwa add_halves at this,
by rw [add_sub_cancel]
lemma add_midpoint {a b : α} (h : a < b) : a + (b - a) / 2 < b :=
begin
rw [← div_sub_div_same, sub_eq_add_neg, add_comm (b/2), ← add_assoc, ← sub_eq_add_neg],
apply add_lt_of_lt_sub_right,
rw [sub_self_div_two, sub_self_div_two],
apply div_lt_div_of_lt_of_pos h two_pos
end
lemma div_two_sub_self (a : α) : a / 2 - a = - (a / 2) :=
suffices a / 2 - (a / 2 + a / 2) = - (a / 2), by rwa add_halves at this,
by rw [sub_add_eq_sub_sub, sub_self, zero_sub]
lemma add_self_div_two (a : α) : (a + a) / 2 = a :=
eq.symm
(iff.mpr (eq_div_iff_mul_eq _ _ (ne_of_gt (add_pos (@zero_lt_one α _) zero_lt_one)))
(begin unfold bit0, rw [left_distrib, mul_one] end))
lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c :=
begin
rw [← mul_div_assoc] at h, rw [mul_comm b],
apply le_mul_of_div_le hc h
end
lemma div_two_lt_of_pos {a : α} (h : a > 0) : a / 2 < a :=
suffices a / (1 + 1) < a, begin unfold bit0, assumption end,
have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one),
calc
a / 2 < a / 2 + a / 2 : lt_add_of_pos_left _ ha
... = a : add_halves a
lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (h : a / b ≤ c / d)
(he : e > 0) : a / (b * e) ≤ c / (d * e) :=
begin
have h₁ := div_mul_eq_div_mul_one_div a b e,
have h₂ := div_mul_eq_div_mul_one_div c d e,
rw [h₁, h₂],
apply mul_le_mul_of_nonneg_right h,
apply le_of_lt,
apply one_div_pos_of_pos he
end
lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 :=
begin
apply exists.intro ((a - b) / (1 + 1)),
split,
{have h2 : a + a > (b + b) + (a - b),
calc
a + a > b + a : add_lt_add_right h _
... = b + a + b - b : by rw add_sub_cancel
... = b + b + a - b : by simp [add_comm, add_left_comm]
... = (b + b) + (a - b) : by rw add_sub,
have h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
exact div_lt_div_of_lt_of_pos h2 two_pos,
rw [one_add_one_eq_two, sub_eq_add_neg],
rw [add_self_div_two, ← div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3,
exact h3},
exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos
end
lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b :=
begin
apply le_of_not_gt,
intro hb,
cases exists_add_lt_and_pos_of_lt hb with c hc,
have hc' := h c (and.right hc),
apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc')
end
lemma one_div_lt_one_div_of_lt {a b : α} (ha : 0 < a) (h : a < b) : 1 / b < 1 / a :=
begin
apply lt_div_of_mul_lt ha,
rw [mul_comm, ← div_eq_mul_one_div],
apply div_lt_of_mul_lt_of_pos (lt_trans ha h),
rwa [one_mul]
end
lemma one_div_le_one_div_of_le {a b : α} (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a :=
(lt_or_eq_of_le h).elim
(λ h, le_of_lt $ one_div_lt_one_div_of_lt ha h)
(λ h, by rw [h])
lemma one_div_lt_one_div_of_lt_of_neg {a b : α} (hb : b < 0) (h : a < b) : 1 / b < 1 / a :=
begin
apply div_lt_of_mul_gt_of_neg hb,
rw [mul_comm, ← div_eq_mul_one_div],
apply div_lt_of_mul_gt_of_neg (lt_trans h hb),
rwa [one_mul]
end
lemma one_div_le_one_div_of_le_of_neg {a b : α} (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a :=
(lt_or_eq_of_le h).elim
(λ h, le_of_lt $ one_div_lt_one_div_of_lt_of_neg hb h)
(λ h, by rw [h])
lemma le_of_one_div_le_one_div {a b : α} (h : 0 < a) (hl : 1 / a ≤ 1 / b) : b ≤ a :=
le_of_not_gt $ λ hn, not_lt_of_ge hl $ one_div_lt_one_div_of_lt h hn
lemma le_of_one_div_le_one_div_of_neg {a b : α} (h : b < 0) (hl : 1 / a ≤ 1 / b) : b ≤ a :=
le_of_not_gt $ λ hn, not_lt_of_ge hl $ one_div_lt_one_div_of_lt_of_neg h hn
lemma lt_of_one_div_lt_one_div {a b : α} (h : 0 < a) (hl : 1 / a < 1 / b) : b < a :=
lt_of_not_ge $ λ hn, not_le_of_gt hl $ one_div_le_one_div_of_le h hn
lemma lt_of_one_div_lt_one_div_of_neg {a b : α} (h : b < 0) (hl : 1 / a < 1 / b) : b < a :=
lt_of_not_ge $ λ hn, not_le_of_gt hl $ one_div_le_one_div_of_le_of_neg h hn
lemma one_div_le_of_one_div_le_of_pos {a b : α} (ha : a > 0) (h : 1 / a ≤ b) : 1 / b ≤ a :=
begin
rw [← one_div_one_div a],
apply one_div_le_one_div_of_le _ h,
apply one_div_pos_of_pos ha
end
lemma one_div_le_of_one_div_le_of_neg {a b : α} (hb : b < 0) (h : 1 / a ≤ b) : 1 / b ≤ a :=
le_of_not_gt $ λ hl, begin
have : a < 0, from lt_trans hl (one_div_neg_of_neg hb),
rw ← one_div_one_div a at hl,
exact not_lt_of_ge h (lt_of_one_div_lt_one_div_of_neg hb hl)
end
lemma one_lt_one_div {a : α} (h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a :=
suffices 1 / 1 < 1 / a, by rwa one_div_one at this,
one_div_lt_one_div_of_lt h1 h2
lemma one_le_one_div {a : α} (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a :=
suffices 1 / 1 ≤ 1 / a, by rwa one_div_one at this,
one_div_le_one_div_of_le h1 h2
lemma one_div_lt_neg_one {a : α} (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1 :=
suffices 1 / a < 1 / -1, by rwa one_div_neg_one_eq_neg_one at this,
one_div_lt_one_div_of_lt_of_neg h1 h2
lemma one_div_le_neg_one {a : α} (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1 :=
suffices 1 / a ≤ 1 / -1, by rwa one_div_neg_one_eq_neg_one at this,
one_div_le_one_div_of_le_of_neg h1 h2
lemma div_lt_div_of_pos_of_lt_of_pos {a b c : α} (hb : 0 < b) (h : b < a) (hc : 0 < c) : c / a < c / b :=
begin
apply lt_of_sub_neg,
rw [div_eq_mul_one_div, div_eq_mul_one_div c b, ← mul_sub_left_distrib],
apply mul_neg_of_pos_of_neg,
exact hc,
apply sub_neg_of_lt,
apply one_div_lt_one_div_of_lt; assumption,
end
lemma div_mul_le_div_mul_of_div_le_div_pos' {a b c d e : α} (h : a / b ≤ c / d)
(he : e > 0) : a / (b * e) ≤ c / (d * e) :=
begin
rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div],
apply mul_le_mul_of_nonneg_right h,
apply le_of_lt,
apply one_div_pos_of_pos he
end
end linear_ordered_field
class discrete_linear_ordered_field (α : Type u) extends linear_ordered_field α,
decidable_linear_ordered_comm_ring α