proposition: Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)).
proof: Proof. by case: d => [|d] // /divnK-Dm; rewrite -[in LHS]Dm divnMBl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)