proposition: Lemma modn_pred m d : d != 1 -> 0 < m -> m.-1 %% d = if d %| m then d.-1 else (m %% d).-1.
proof: Proof. rewrite -subn1; case: d m => [|[|d]] [|m]//= _ _. by rewrite ?modn1 ?dvd1n ?modn0 ?subn1. rewrite modnB// (@modn_small 1)// [_ < _]leqn0 /dvdn mulnbl/= subn1. by case: eqP => // ->; rewrite addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)