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.