mathcompbook_edivn.v

From mathcomp Require Import all_ssreflect.

Fixpoint evivn_rec pred_d m q :=
  if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m).

Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).

Lemma edivn_recP1 q r m pred_d q0:
  (q, r) = edivn_rec pred_d m q0 ->
  r < pred_d.+1.
Proof.
case (ubnPgeq m). elim: m q0 => [|m IHm] q0 [/=|n] leqnm // []; try move=> _ -> //.
simpl. rewrite subn_if_gt. case: ifP=> cond []; last first.
- move=> _ ->. by rewrite ltnS ltnNge cond.
- by apply: IHm; rewrite (@leq_trans n) // leq_subr.
Qed.

Lemma edivn_recP2 q r m pred_d q0 :
  (q, r) = edivn_rec pred_d m q0 ->
  q0 * pred_d.+1 + m =  q * pred_d.+1 + r.
Proof.
case (ubnPgeq m). elim: m q0 => [|m IHm] q0 [/=|n] leqnm // []; try by move=> -> ->.
simpl. rewrite subn_if_gt. case: ifP=> cond // []; last by move=> -> ->.
move=> qr. rewrite -(IHm q0.+1 (n-pred_d)) //.
- by rewrite mulSnr -addnA addSn subnKC.
- by rewrite (@leq_trans n) // leq_subr.
Qed.

Lemma edivnP1 q r m d :
  (q, r) = edivn m d -> d > 0 -> r < d.
Proof.
by case d=> // n /= qr _; apply/edivn_recP1/qr.
Qed.

Lemma edivnP2 q r m d :
  (q, r) = edivn m d -> m = q * d + r.
Proof.
rewrite /edivn. case d => /= [[] -> -> |n qr] //.
by rewrite -(edivn_recP2 _ _ m _ 0) //.
Qed.