Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** Additional lemmas about [divn] and [modn]. *) Section DivMod. (** First, we show that if [t1 / h] is equal to [t2 / h] and [t1 <= t2], then [t1 mod h] is bounded by [t2 mod h]. *)

forall t1 t2 h : nat, t1 <= t2 -> t1 %/ h = t2 %/ h -> t1 %% h <= t2 %% h

forall t1 t2 h : nat, t1 <= t2 -> t1 %/ h = t2 %/ h -> t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h

t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
Z: h = 0

t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h
t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
Z: h = 0

t1 %% h <= t2 %% h
by subst; rewrite !modn0.
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h

t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h

t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h

exists k : nat, t1 + k = t2
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h
EX: exists k : nat, t1 + k = t2
t1 %% h <= t2 %% h
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h

exists k : nat, t1 + k = t2
exists (t2 - t1); lia.
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
POSh: 0 < h
EX: exists k : nat, t1 + k = t2

t1 %% h <= t2 %% h
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h

t1 %% h <= (t1 + k) %% h
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h

false = (h <= t1 %% h + k %% h)
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h

t1 %% h + k %% h < h
t1, h, k: nat
POSh: 0 < h

t1 %/ h + k %/ h + (h <= t1 %% h + k %% h) == t1 %/ h -> t1 %% h + k %% h < h
t1, h, k: nat
POSh: 0 < h
Z2: (h <= t1 %% h + k %% h) = 0

t1 %% h + k %% h < h
by move: Z2 => /eqP; rewrite eqb0 -ltnNge. } Qed. (** Given two natural numbers [x] and [y], the fact that [x / y < (x + 1) / y] implies that [y] divides [x + 1]. *)

forall x y : nat, x %/ y < (x + 1) %/ y -> y %| x + 1

forall x y : nat, x %/ y < (x + 1) %/ y -> y %| x + 1
x, y: nat
LT: x %/ y < (x + 1) %/ y

y %| x + 1
x, y: nat
LT: x %/ y < (x + 1) %/ y
POS: 0 < y

y %| x + 1
x, y: nat
POS: 0 < y
ONE: 0 < 1 %/ y

y %| x + 1
x, y: nat
POS: 0 < y
LE: 0 < (y <= x %% y + 1 %% y)
y %| x + 1
x, y: nat
POS: 0 < y
ONE: 0 < 1 %/ y

y %| x + 1
by destruct y as [ | []].
x, y: nat
POS: 0 < y
LE: 0 < (y <= x %% y + 1 %% y)

y %| x + 1
x, y: nat
POS: 0 < y
LE: 0 < (y <= x %% y + 1 %% y)

y %| x + 1
x, y: nat
POS: 0 < y
LE: y <= x %% y + 1 %% y

y %| x + 1
x, y: nat
POS: 0 < y
LE: y <= x %% y + 1 %% y
LT2: 1 < y

y %| x + 1
x, y: nat
LT2: 1 < y
LE: y <= x %% y + 1

y %| x + 1
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| x + 1
x, y: nat
LT2: 1 < y
LT: y < x %% y + 1
y %| x + 1
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| x + 1
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| x %/ y * y
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1
y %| y
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| x %/ y * y
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1
y %| y
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| y
x, y: nat
LT2: 1 < y
EQ: y = x %% y + 1

y %| y
by apply dvdnn.
x, y: nat
LT2: 1 < y
LT: y < x %% y + 1

y %| x + 1
x, y: nat
LT2: 1 < y
LT: y < x %% y + 1

y %| x + 1
by move: LT; rewrite -addn1 leq_add2r leqNgt ltn_pmod //; lia. } } Qed. (** We prove an auxiliary lemma allowing us to change the order of operations [_ + 1] and [_ %% h]. *)

forall x h : nat, 0 < h -> x %/ h = (x + 1) %/ h -> (x + 1) %% h = x %% h + 1

forall x h : nat, 0 < h -> x %/ h = (x + 1) %/ h -> (x + 1) %% h = x %% h + 1
x, h: nat
POS: 0 < h
EQ: x %/ h = (x + 1) %/ h

(x + 1) %% h = x %% h + 1
x, h: nat
POS: 0 < h
EQ: x %/ h = (x + 1) %/ h

x.+1 %% h = (x %% h).+1
x, h: nat
POS: 0 < h
EQ: x %/ h = (h %| x.+1) + x %/ h

x.+1 %% h = (x %% h).+1
x, h: nat
POS: 0 < h
DIV: (h %| x.+1) = false
EQ: x %/ h = 0 + x %/ h

x.+1 %% h = (x %% h).+1
by rewrite modnS DIV. Qed. (** We show that the fact that [x / h = (x + y) / h] implies that [h] is larder than [x mod h + y mod h]. *)

forall x y h : nat, 0 < h -> x %/ h = (x + y) %/ h -> x %% h + y %% h < h

forall x y h : nat, 0 < h -> x %/ h = (x + y) %/ h -> x %% h + y %% h < h
x, y, h: nat
POS: 0 < h
EQ: x %/ h = (x + y) %/ h

x %% h + y %% h < h
x, y, h: nat
POS: 0 < h
Z1: y %/ h = 0
Z2: (h <= x %% h + y %% h) = 0

x %% h + y %% h < h
by move: Z2 => /eqP; rewrite eqb0 -ltnNge => LT. Qed. End DivMod. (** In this section, we define notions of [div_floor] and [div_ceil] and prove a few basic lemmas. *) Section DivFloorCeil. (** We define functions [div_floor] and [div_ceil], which are divisions rounded down and up, respectively. *) Definition div_floor (x y : nat) : nat := x %/ y. Definition div_ceil (x y : nat) := if y %| x then x %/ y else (x %/ y).+1. (** We start with an observation that [div_ceil 0 b] is equal to [0] for any [b]. *)

forall b : nat, div_ceil 0 b = 0

forall b : nat, div_ceil 0 b = 0
b: nat

(if b %| 0 then 0 %/ b else (0 %/ b).+1) = 0
by rewrite dvdn0; apply div0n. Qed. (** Next, we show that, given two positive integers [a] and [b], [div_ceil a b] is also positive. *)

forall a b : nat, 0 < a -> 0 < b -> 0 < div_ceil a b

forall a b : nat, 0 < a -> 0 < b -> 0 < div_ceil a b
a, b: nat
POSa: 0 < a
POSb: 0 < b

0 < div_ceil a b
a, b: nat
POSa: 0 < a
POSb: 0 < b

0 < (if b %| a then a %/ b else (a %/ b).+1)
a, b: nat
POSa: 0 < a
POSb: 0 < b
EQ: (b %| a) = true

0 < a %/ b
by rewrite divn_gt0 //; apply dvdn_leq. Qed. (** We show that [div_ceil] is monotone with respect to the first argument. *)

forall d m n : nat, m <= n -> div_ceil m d <= div_ceil n d

forall d m n : nat, m <= n -> div_ceil m d <= div_ceil n d
d, m, n: nat
LEQ: m <= n

div_ceil m d <= div_ceil n d
d, m, n: nat
LEQ: m <= n

(if d %| m then m %/ d else (m %/ d).+1) <= (if d %| n then n %/ d else (n %/ d).+1)
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d

(if d %| m then m %/ d else (m %/ d).+1) <= (if d %| n then n %/ d else (n %/ d).+1)
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true

m %/ d < n %/ d
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true

m %/ d * d < n
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true

m %/ d * d < m
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
LEQm: m %/ d * d <= m

m %/ d * d < m
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
LEQm: true
e: m %/ d * d = m

false
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
LEQm: true
EQ: d %| m

false
by rewrite EQ in Mm. Qed. (** Given [T] and [Δ] such that [Δ >= T > 0], we show that [div_ceil Δ T] is strictly greater than [div_ceil (Δ - T) T]. *)

forall Δ T : nat, 0 < T -> T <= Δ -> div_ceil (Δ - T) T < div_ceil Δ T

forall Δ T : nat, 0 < T -> T <= Δ -> div_ceil (Δ - T) T < div_ceil Δ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ

div_ceil (Δ - T) T < div_ceil Δ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < (if T %| Δ then Δ %/ T else (Δ %/ T).+1)
Δ, T: nat
POS: 0 < T
LE: T <= Δ

(Δ - T) %/ T < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < (if T %| Δ then Δ %/ T else (Δ %/ T).+1)
Δ, T: nat
POS: 0 < T
LE: T <= Δ

(Δ - T) %/ T < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ

Δ %/ T - T %/ T < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ

Δ %/ T - true < Δ %/ T
rewrite ltn_psubCl //; lia.
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < (if T %| Δ then Δ %/ T else (Δ %/ T).+1)
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = true

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = false
(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < (Δ %/ T).+1
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = true

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = true
divck: T %| Δ -> T %| Δ - T

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < Δ %/ T
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = true
divck: T %| Δ -> T %| Δ - T
EQ2: T %| Δ - T

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < Δ %/ T
rewrite EQ2; apply lkc.
Δ, T: nat
POS: 0 < T
LE: T <= Δ
lkc: (Δ - T) %/ T < Δ %/ T
EQ1: (T %| Δ) = false

(if T %| Δ - T then (Δ - T) %/ T else ((Δ - T) %/ T).+1) < (Δ %/ T).+1
by destruct (T %| Δ - T) eqn:EQ, (T %| Δ) eqn:EQ3; auto. Qed. (** We show that the division with ceiling by a constant [T] is a subadditive function. *)

forall T : nat, subadditive (div_ceil^~ T)

forall T : nat, subadditive (div_ceil^~ T)
T, ab, a, b: nat
SUM: a + b = ab

div_ceil ab T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = true
DIVab: T %| a + b

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = true
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = true
DIVab: (T %| a + b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = true

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = true

(a + b) %/ T <= (a %/ T).+1 + (b %/ T).+1
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = true

(a + b) %/ T <= a %/ T + b %/ T + 1
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false

div_ceil (a + b) T <= div_ceil a T + div_ceil b T
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false

(a + b) %/ T < (a %/ T).+1 + (b %/ T).+1
T, ab, a, b: nat
SUM: a + b = ab
DIVa: (T %| a) = false
DIVb: (T %| b) = false
DIVab: (T %| a + b) = false

(a + b) %/ T <= a %/ T + b %/ T + 1
by apply leq_divDl. Qed. (** We observe that when dividing a value exceeding [T * n], then the ceiling exceeds [n]. *)

forall Δ T n : nat, 0 < T -> T * n < Δ -> n < div_ceil Δ T

forall Δ T n : nat, 0 < T -> T * n < Δ -> n < div_ceil Δ T
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta

n < div_ceil delta T
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta

n < (if T %| delta then delta %/ T else (delta %/ T).+1)
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta
DIV: (T %| delta) = false

n < (delta %/ T).+1
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta
DIV: (T %| delta) = false

T * n < (delta + T) %/ T * T
by lia. Qed. (** We show that for any two integers [a] and [b], [a] is less than [a %/ b * b + b] given that [b] is positive. *)

forall a b : nat, 0 < b -> a < a %/ b * b + b

forall a b : nat, 0 < b -> a < a %/ b * b + b
a, b: nat
POS: 0 < b

a < a %/ b * b + b
a, b: nat
POS: 0 < b
DIV: a = a %/ b * b + a %% b

a < a %/ b * b + b
a, b: nat
POS: 0 < b
DIV: a = a %/ b * b + a %% b

a %/ b * b + a %% b < a %/ b * b + b
a, b: nat
POS: 0 < b
DIV: a = a %/ b * b + a %% b

a %% b < b
by apply ltn_pmod. Qed. (** We prove a technical lemma stating that for any three integers [a, b, c] such that [c > b], [mod] can be swapped with subtraction in the expression [(a + c - b) %% c]. *)

forall a b c : nat, b < c -> (a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)

forall a b c : nat, b < c -> (a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
a, b, c: nat
BC: b < c

(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
a, b, c: nat
BC: b < c
POS: 0 < c

(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c

(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = true

(a %% c + (c - b)) %% c = a %% c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = false
(a %% c + (c - b)) %% c = a %% c + c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = true

(a %% c + (c - b)) %% c = a %% c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = false
(a %% c + (c - b)) %% c = a %% c + c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = true

(a %% c - b + c) %% c = a %% c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = false
(a %% c + (c - b)) %% c = a %% c + c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = false

(a %% c + (c - b)) %% c = a %% c + c - b
a, b, c: nat
BC: b < c
POS: 0 < c
G: a %% c < c
CASE: (b <= a %% c) = false

(a %% c + (c - b)) %% c = a %% c + c - b
by rewrite modn_small; lia. Qed. End DivFloorCeil.