Library prosa.util.div_mod


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


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

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 25)
  
  ============================
  forall a b c : nat,
  0 < c ->
  b < c ->
  (a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)

----------------------------------------------------------------------------- *)


Proof.
  intros× CP BC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  a, b, c : nat
  CP : 0 < c
  BC : b < 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 34)
  
  a, b, c : nat
  CP : 0 < c
  BC : b < 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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 72)
  
  a, b, c : nat
  CP : 0 < c
  BC : b < c
  G : a %% c < c
  CASE : (b <= a %% c) = true
  ============================
  (a %% c + (c - b)) %% c = a %% c - b

subgoal 2 (ID 77) is:
 (a %% c + (c - b)) %% c = a %% c + c - b

----------------------------------------------------------------------------- *)


  - rewrite add_subC;auto.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 84)
  
  a, b, c : nat
  CP : 0 < c
  BC : b < c
  G : a %% c < c
  CASE : (b <= a %% c) = true
  ============================
  (a %% c - b + c) %% c = a %% c - b

subgoal 2 (ID 77) is:
 (a %% c + (c - b)) %% c = a %% c + c - b

----------------------------------------------------------------------------- *)


rewrite -modnDmr modnn addn0 modn_small;auto;ssromega.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  a, b, c : nat
  CP : 0 < c
  BC : b < c
  G : a %% c < c
  CASE : (b <= a %% c) = false
  ============================
  (a %% c + (c - b)) %% c = a %% c + c - b

----------------------------------------------------------------------------- *)


  - rewrite modn_small;try ssromega.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.