proposition: Lemma shift_mod_n_vl n k i: natp n -> n <> \0c -> k <c n -> i<c n -> ((i +c k) %%c n) = Yo (i +c k <c n) (i +c k) ((i +c k) -c n).
proof: Proof. move => nN nz kn iin. move: (NS_le_nat (proj1 kn) nN) => kN. move: (NS_le_nat (proj1 iin) nN) => iN. move: (NS_sum iN kN) => sN. case: (cleT_el (CS_nat nN) (CS_nat sN)) => le1. move: (cdiff_pr le1) => aux. move: (NS_diff n sN) => dN. have h: cdivision_prop (i +c k) n \1c ((i +c k) -c n). split; first by rewrite (cprod1r (CS_nat nN)). apply : (csum_lt2l nN dN nN). rewrite aux; exact (csum_Mlelt nN (proj1 iin) kn). by rewrite (Y_false (cleNgt le1)) - (proj2 (cquorem_pr sN nN NS1 dN h)). have h: cdivision_prop (i +c k) n \0c (i +c k). by split => //; rewrite cprod0r csum0l; fprops. by Ytac0; rewrite -(proj2 (cquorem_pr sN nN NS0 sN h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)