proposition: Lemma shift_mod_n_fb n k: natp n -> n <> \0c -> k <c n -> bijection (shift_mod_n n k).
proof: Proof. move => nN nz kn. move: (NS_le_nat (proj1 kn) nN) => kN. apply: lf_bijective. by apply: shift_mod_n_ax. move => u v /(NintP nN) un /(NintP nN) vn. rewrite (shift_mod_n_vl nN nz kn un). rewrite (shift_mod_n_vl nN nz kn vn) => le0. move: (NS_le_nat (proj1 un) nN) => uN. move: (NS_le_nat (proj1 vn) nN) => vN. apply: (csum_eq2r kN uN vN). move: (NS_sum uN kN) (NS_sum vN kN) => suN svN. move: (cleT_el (CS_nat nN) (CS_nat svN)) => cs. move: le0. case: (cleT_el (CS_nat nN) (CS_nat suN)) => le1. rewrite (Y_false (cleNgt le1)). case: cs => le2. rewrite (Y_false (cleNgt le2)) => eq1. move: (f_equal (csum2 n) eq1). by rewrite (cdiff_pr le1) (cdiff_pr le2). Ytac0 => eq1; move: (f_equal (csum2 n) eq1). rewrite (cdiff_pr le1) csumA => le3. move: (Nsum_M0le v nN). by rewrite -(csum_eq2r kN uN (NS_sum nN vN) le3) => /(cltNge un). Ytac0; case: cs => le2; last by Ytac0. rewrite (Y_false (cleNgt le2)) => eq1. move: (f_equal (csum2 n) eq1); rewrite (cdiff_pr le2) csumA => le3. move: (Nsum_M0le u nN); symmetry in le3. by rewrite -(csum_eq2r kN vN (NS_sum nN uN) le3) => /(cltNge vn). move => y /(NintP nN) yn. move: (NS_le_nat (proj1 yn) nN) => yN. move:(Nsum_Mle0 y nN) => le2. case: (cleT_el (CS_nat kN) (CS_nat yN)) => le1. move: (cdiff_pr le1) => qa. have lt1:= (cle_ltT (cdiff_ab_le_a k (CS_nat yN)) yn). exists (y -c k); first by apply /(NintP nN). by rewrite (shift_mod_n_vl nN nz kn lt1) csumC qa; Ytac0. have kyn:= cleT (proj1 kn) le2. move: (cdiff_pr kyn) => eq1. move: (NS_diff k (NS_sum yN nN)) => dN. have lt1: (y +c n) -c k <c n. apply : (csum_lt2l kN dN nN); rewrite eq1. by apply: csum_Mlteq. exists ((y +c n) -c k); first by apply /(NintP nN). rewrite (shift_mod_n_vl nN nz kn lt1). by rewrite csumC in eq1; rewrite eq1 (Y_false (cleNgt le2)) cdiff_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)