proposition: Lemma divides_frac_diff {m n} : m mod (n + 1) = 0 -> (m * (n + 2) / (n + 1) - m) * (1 + n) = m.
proof: Proof. rewrite Nat.mul_sub_distr_r. move=> /div_exact => ?. have -> : m * (n + 2) = ((n+2) * (m / (n + 1))) * (n + 1) by lia. by rewrite Nat.div_mul; lia. Qed.
imports: Arith Lia ZArith.Znat ZArith.Zdiv ssreflect ssrbool ssrfun