Library prosa.util.div_mod

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 :
     t1 t2 h,
      t1 t2
      t1 %/ h = t2 %/ h
      t1 %% h t2 %% h.

Given two natural numbers x and y, the fact that x / y < (x + 1) / y implies that y divides x + 1.
  Lemma ltdivn_dvdn :
     x y,
      x %/ y < (x + 1) %/ y
      y %| (x + 1).
We prove an auxiliary lemma allowing us to change the order of operations _ + 1 and _ %% h.
  Lemma addn1_modn_commute :
     x h,
      h > 0
      x %/ h = (x + 1) %/ h
      (x + 1) %% h = x %% h + 1 .

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 :
     x y h,
      h > 0
      x %/ h = (x + y) %/ h
      h > x %% h + y %% h.

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:
     b, div_ceil 0 b = 0.

Next, we show that, given two positive integers a and b, div_ceil a b is also positive.
  Lemma div_ceil_gt0:
     a b,
      a > 0 b > 0
      div_ceil a b > 0.

We show that div_ceil is monotone with respect to the first argument.
  Lemma div_ceil_monotone1:
     d m n,
      m n div_ceil m d div_ceil n d.

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:
     Δ T,
      T > 0 Δ T
      div_ceil (Δ - T) T < div_ceil Δ T.

We show that the division with ceiling by a constant T is a subadditive function.
  Lemma div_ceil_subadditive:
     T, subadditive (div_ceil^~T).

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:
     a b,
      b > 0
      a < a %/ b × b + b.

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:
     a b c,
      c > b
      (a + c - b) %% c = if a %% c b then (a %% c - b) else (a %% c + c - b).

End DivFloorCeil.