From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.util.nat prosa.util.subadditivity.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

(** 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]. *)
  Lemma eqdivn_leqmodn :
    forall t1 t2 h,
      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
  Proof.
forall t1 t2 h : nat,
t1 <= t2 -> t1 %/ h = t2 %/ h -> t1 %% h <= t2 %% h
    move=> t1 t2 h LT EQ.
t1, t2, h: nat
LT: t1 <= t2
EQ: t1 %/ h = t2 %/ h
t1 %% h <= t2 %% h
    destruct (posnP h) as [Z | POSh].
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 have EX: exists k, t1 + k = t2.
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
      destruct EX as [k EX]; subst t2; clear LT.
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h
t1 %% h <= (t1 + k) %% h
      rewrite modnD //; replace (h <= t1 %% h + k %% h) with false; first by lia.
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h
false = (h <= t1 %% h + k %% h)
      symmetry; apply/negP/negP; rewrite -ltnNge.
t1, h, k: nat
EQ: t1 %/ h = (t1 + k) %/ h
POSh: 0 < h
t1 %% h + k %% h < h
      symmetry in EQ; rewrite divnD // in EQ; move: EQ => /eqP.
t1, h, k: nat
POSh: 0 < h
t1 %/ h + k %/ h + (h <= t1 %% h + k %% h) == t1 %/ h ->
t1 %% h + k %% h < h
      rewrite -{2}[t1 %/ h]addn0 -addnA eqn_add2l addn_eq0 => /andP [_ /eqP Z2].
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]. *)
  Lemma ltdivn_dvdn :
    forall x y,
      x %/ y < (x + 1) %/ y -> 
      y %| (x + 1).
forall x y : nat, x %/ y < (x + 1) %/ y -> y %| x + 1
  Proof.
forall x y : nat, x %/ y < (x + 1) %/ y -> y %| x + 1
    move=> x y LT.
x, y: nat
LT: x %/ y < (x + 1) %/ y
y %| x + 1
    destruct (posnP y) as [Z | POS]; first by subst y.
x, y: nat
LT: x %/ y < (x + 1) %/ y
POS: 0 < y
y %| x + 1
    move: LT; rewrite divnD // -addn1 -addnA leq_add2l addn_gt0 => /orP [ONE | LE].
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 rewrite lt0b in LE.
x, y: nat
POS: 0 < y
LE: y <= x %% y + 1 %% y
y %| x + 1 
      destruct (leqP 2 y) as [LT2 | GE2]; last by destruct y as [ | []].
x, y: nat
POS: 0 < y
LE: y <= x %% y + 1 %% y
LT2: 1 < y
y %| x + 1
      clear POS; rewrite [1 %%  _]modn_small // in LE.
x, y: nat
LT2: 1 < y
LE: y <= x %% y + 1
y %| x + 1
      move: LE; rewrite leq_eqVlt => /orP [/eqP EQ | LT].
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 rewrite [x](divn_eq x y) -addnA -EQ; apply dvdn_add.
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 by apply dvdn_mull, dvdnn.
        -
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]. *) 
  Lemma addn1_modn_commute :
    forall x h,
      h > 0 -> 
      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
  Proof.
forall x h : nat,
0 < h ->
x %/ h = (x + 1) %/ h -> (x + 1) %% h = x %% h + 1
    intros x h POS EQ.
x, h: nat
POS: 0 < h
EQ: x %/ h = (x + 1) %/ h
(x + 1) %% h = x %% h + 1
    rewrite !addnS !addn0.
x, h: nat
POS: 0 < h
EQ: x %/ h = (x + 1) %/ h
x.+1 %% h = (x %% h).+1
    rewrite addnS divnS // addn0 in EQ.
x, h: nat
POS: 0 < h
EQ: x %/ h = (h %| x.+1) + x %/ h
x.+1 %% h = (x %% h).+1
    destruct (h %| x.+1) eqn:DIV ; rewrite /= in EQ; first by lia.
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]. *)
  Lemma addmod_le_mod :
    forall x y h,
      h > 0 -> 
      x %/ h = (x + y) %/ h ->
      h > x %% h + y %% h.
forall x y h : nat,
0 < h -> x %/ h = (x + y) %/ h -> x %% h + y %% h < h
  Proof.
forall x y h : nat,
0 < h -> x %/ h = (x + y) %/ h -> x %% h + y %% h < h
    intros x y h POS EQ.
x, y, h: nat
POS: 0 < h
EQ: x %/ h = (x + y) %/ h
x %% h + y %% h < h
    move: EQ => /eqP; rewrite divnD // -{1}[x %/ h]addn0 -addnA eqn_add2l eq_sym addn_eq0 => /andP [/eqP Z1 /eqP Z2].
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]. *) 
  Lemma div_ceil0:
    forall b, div_ceil 0 b = 0.
forall b : nat, div_ceil 0 b = 0
  Proof.
forall b : nat, div_ceil 0 b = 0
    intros b; unfold div_ceil.
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. *)
  Lemma div_ceil_gt0:
    forall a b,
      a > 0 -> b > 0 ->
      div_ceil a b > 0.
forall a b : nat, 0 < a -> 0 < b -> 0 < div_ceil a b
  Proof.
forall a b : nat, 0 < a -> 0 < b -> 0 < div_ceil a b
    intros a b POSa POSb.
a, b: nat
POSa: 0 < a
POSb: 0 < b
0 < div_ceil a b
    unfold div_ceil.
a, b: nat
POSa: 0 < a
POSb: 0 < b
0 < (if b %| a then a %/ b else (a %/ b).+1)
    destruct (b %| a) eqn:EQ; last by done.
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. *)
  Lemma div_ceil_monotone1:
    forall d m n,
      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
  Proof.
forall d m n : nat,
m <= n -> div_ceil m d <= div_ceil n d
    move => d m n LEQ.
d, m, n: nat
LEQ: m <= n
div_ceil m d <= div_ceil n d
    rewrite /div_ceil.
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)
    have LEQd: m %/ d <= n %/ d by apply leq_div2r.
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)
    destruct (d %| m) eqn:Mm; destruct (d %| n) eqn:Mn => //; first by lia.
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
m %/ d < n %/ d
    rewrite ltn_divRL //.
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
m %/ d * d < n
    apply: (leq_trans _ LEQ).
d, m, n: nat
LEQ: m <= n
LEQd: m %/ d <= n %/ d
Mm: (d %| m) = false
Mn: (d %| n) = true
m %/ d * d < m
    move: (leq_trunc_div m d) => LEQm.
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
    destruct (ltngtP (m %/ d * d) m) as [| |e] => //.
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
    move: e => /eqP EQ; rewrite -dvdn_eq in EQ.
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]. *)
  Lemma leq_div_ceil_add1:
    forall Δ T,
      T > 0 -> Δ >= T ->
      div_ceil (Δ - T) T < div_ceil Δ T.
forall Δ T : nat,
0 < T -> T <= Δ -> div_ceil (Δ - T) T < div_ceil Δ T
  Proof.
forall Δ T : nat,
0 < T -> T <= Δ -> div_ceil (Δ - T) T < div_ceil Δ T
    move=> Δ T POS LE.
Δ, T: nat
POS: 0 < T
LE: T <= Δ
div_ceil (Δ - T) T < div_ceil Δ T rewrite /div_ceil.
Δ, T: nat
POS: 0 < T
LE: T <= Δ
(if T %| Δ - T
 then (Δ - T) %/ T
 else ((Δ - T) %/ T).+1) <
(if T %| Δ then Δ %/ T else (Δ %/ T).+1)
    have lkc: (Δ - T) %/ T < Δ %/ T.
Δ, 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 rewrite divnBr; last by auto.
Δ, T: nat
POS: 0 < T
LE: T <= Δ
Δ %/ T - T %/ T < Δ %/ T
      rewrite divnn POS.
Δ, 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)
    destruct (T %| Δ) eqn:EQ1.
Δ, 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 have divck:  (T %| Δ) ->  (T %| (Δ - T)) by auto.
Δ, 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
      apply divck in EQ1 as EQ2.
Δ, 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. *)
  Lemma div_ceil_subadditive:
    forall T, subadditive (div_ceil^~T).
forall T : nat, subadditive (div_ceil^~ T)
  Proof.
forall T : nat, subadditive (div_ceil^~ T)
    move=> T ab a b SUM.
T, ab, a, b: nat
SUM: a + b = ab
div_ceil ab T <= div_ceil a T + div_ceil b T
    rewrite -SUM.
T, ab, a, b: nat
SUM: a + b = ab
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
    destruct (T %| a) eqn:DIVa, (T %| b) eqn:DIVb.
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 have DIVab: T %| a + b by apply dvdn_add.
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
      by rewrite /div_ceil DIVa DIVb DIVab divnDl.
    -
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 have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
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
      by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; lia.
    -
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 have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
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
      by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; lia.
    -
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 destruct (T %| a + b) eqn:DIVab.
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 rewrite /div_ceil DIVa DIVb DIVab.
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
        apply leq_trans with (a %/ T + b %/T + 1); last by lia.
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
        by apply leq_divDl.
      +
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 rewrite /div_ceil DIVa DIVb DIVab.
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
        apply leq_ltn_trans with (a %/ T + b %/T + 1); last by lia.
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]. *)
  Lemma div_ceil_multiple :
    forall Δ T n,
      T > 0 ->
      (T * n) < Δ ->
      n < div_ceil Δ T.
forall Δ T n : nat,
0 < T -> T * n < Δ -> n < div_ceil Δ T
  Proof.
forall Δ T n : nat,
0 < T -> T * n < Δ -> n < div_ceil Δ T
    move=> delta T n GT0 LT.
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta
n < div_ceil delta T
    rewrite /div_ceil.
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta
n <
(if T %| delta then delta %/ T else (delta %/ T).+1)
    case DIV: (T %| delta);
      first by rewrite -(ltn_pmul2l GT0) [_ * (_ %/ _)]mulnC divnK.
delta, T, n: nat
GT0: 0 < T
LT: T * n < delta
DIV: (T %| delta) = false
n < (delta %/ T).+1
    rewrite -[(_ %/ _).+1]addn1  -divnDMl // -(ltn_pmul2l GT0) [_ * (_ %/ _)]mulnC mul1n.
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. *)
  Lemma div_floor_add_g:
    forall a b,
      b > 0 ->
      a < a %/ b * b + b.
forall a b : nat, 0 < b -> a < a %/ b * b + b
  Proof.
forall a b : nat, 0 < b -> a < a %/ b * b + b
    move=> a b POS.
a, b: nat
POS: 0 < b
a < a %/ b * b + b
    specialize (divn_eq a b) => DIV.
a, b: nat
POS: 0 < b
DIV: a = a %/ b * b + a %% b
a < a %/ b * b + b
    rewrite [in X in X < _]DIV.
a, b: nat
POS: 0 < b
DIV: a = a %/ b * b + a %% b
a %/ b * b + a %% b < a %/ b * b + b
    rewrite ltn_add2l.
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]. *) 
  Lemma mod_elim:
    forall a b c,
      c > b ->
      (a + c - b) %% c = if a %% c >= b 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)
  Proof.
forall a b c : nat,
b < c ->
(a + c - b) %% c =
(if b <= a %% c then a %% c - b else a %% c + c - b)
    move=> a b c BC.
a, b, c: nat
BC: b < c
(a + c - b) %% c =
(if b <= a %% c then a %% c - b else a %% c + c - b)
    have POS : c > 0 by lia.
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)
    have G : a %% c < c by apply ltn_pmod.
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)
    case (b <= a %% c) eqn:CASE; rewrite -addnBA; auto; rewrite -modnDml.
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 rewrite addnABC; auto.
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
      by rewrite -modnDmr modnn addn0 modn_small; auto; lia.
    -
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.