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.