Library prosa.classic.util.div_mod

Require Export prosa.util.div_mod.

Require Import Arith Nat.
Require Import prosa.classic.util.tactics mathcomp.zify.zify prosa.classic.util.nat.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

  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.

  Lemma ltn_div_trunc :
     m n d,
      d > 0
      m %/ d < n %/ d
      m < n.

  Lemma subndiv_eq_mod:
     n d, n - n %/ d × d = n %% d.

  Lemma divSn_cases :
     n d,
      d > 1
      (n %/ d = n.+1 %/d n %% d + 1 = n.+1 %% d)
      (n %/ d + 1 = n.+1 %/ d).

  Lemma ceil_neq0 :
     x y,
      x > 0
      y > 0
      div_ceil x y > 0.

  Lemma leq_divceil2r :
     d m n,
      d > 0
      m n
      div_ceil m d div_ceil n d.

(* Versions of eqn_modDl and eqn_modDl in Prop *)

  Lemma eq_modDl: p m n d, (p + m = p + n %[mod d]) (m = n %[mod d]).

  Lemma eq_modDr: p m n d, (m + p = n + p %[mod d]) (m = n %[mod d]).

  (* If a(n)= b+a (n) then b is a multiple of c 
    Proposed name modnD_k *)


  Lemma modulo_exists: a b c,
    c>0 a = b + a %[mod c] k, b = k×c.

  (* If (a+1)n+1=0 then an+1=n *)
  Lemma modnS_eq : a n, a.+1 %% n.+1 =0 a %% n.+1 = n.

  (* Incrementing the integer under a modulo either increments the result or yields 0 *)

  Lemma modnSor': a n, a.+1 %% n = (a %% n).+1 (a.+1 %% n =0).

  Lemma modnSor: a n, a.+1 %% n.+1 = (a %% n.+1).+1 (a.+1 %% n.+1 =0).

  (* Old version of the lemma which is now covered by modnSor and modnS_eq *)

  Lemma modulo_cases : a c,
    a.+1 %% c.+1 = (a %% c.+1).+1 (a.+1 %% c.+1 =0 a %% c.+1 =c).

  Lemma ceil_eq1: a c, a > 0 a c div_ceil a c = 1.

  Lemma ceil_suba: a c, c > 0 a > c div_ceil a c = (div_ceil (a-c) c).+1.

  Lemma mod_eq: a b, a%%b = a - a%/b × b.