proposition: Lemma shift_mod_n_ax n k: natp n -> n <> \0c -> natp k -> forall i, inc i (Nint n) -> inc ((i +c k) %%c n) (Nint n).
proof: Proof. move => nN nz kB i /(NintP nN) => iin; apply /(NintP nN). apply: crem_pr => //; apply: NS_sum => //. apply: (NS_le_nat (proj1 iin) nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)