proposition: Lemma ex4 a b n : a > 0 -> b > 0 -> n > 0 -> edivn (a * b ^ n - 1) (b ^ n.+1) = ((a - 1) %/ b, ((a - 1) %% b) * b ^ n + b ^ n - 1).
proof: Proof. move=> a_gt0 b_gt0 n_gt0; rewrite /divn modn_def. have [q r aB1_eq r_lt] /= := edivnP (a - 1). rewrite b_gt0 /= in r_lt. have /(congr1 (muln^~ (b ^ n))) := aB1_eq. rewrite mulnBl mulnDl mul1n. move=> /(congr1 (addn^~ (b ^ n - 1))). rewrite addnBA ?expn_gt0 ?b_gt0// subnK; last first. by rewrite -[X in X <= _]mul1n leq_mul2r a_gt0 orbT. rewrite -mulnA -expnS -addnA => ->. rewrite edivn_eq addnBA ?expn_gt0 ?b_gt0//. rewrite subnS subn0 prednK ?addn_gt0 ?expn_gt0 ?b_gt0 ?orbT//. rewrite -[X in _ + X]mul1n -mulnDl addn1 expnS. by rewrite leq_mul2r r_lt orbT. Qed.
imports: mathcomp(all_ssreflect)