proposition: Lemma eqmod_contraction_rep9 a (x := contraction_rep \10c a) (y := a %%c \9c) : natp a -> [/\ a = x %c[mod \9c], (a = \0c -> x = \0c) & (a <> \0c -> (y = \0c -> x = \9c) /\ (y <> \0c -> x = y))].
proof: Proof. move => an. apply:eqmod_contraction_rep => //; [ apply:NS9 | apply: card9_nz]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)