proposition: Lemma opp_seq_p3 A n a b: intp n -> natp a -> natp b -> csumb (ZN_int n a b) (Vg A) = csumb (ZN_int (BZopp n) b a) (Vg (opp_seq A)).
proof: Proof. move => nz aN bN. move: (ZSo nz) => mz. set I := (ZN_int (BZopp n) b a). set J := (ZN_int n a b). have Iz i: inc i I -> intp i by move /(ZN_intP mz bN aN)/ proj1 /proj32. move: (ZNz aN) (ZNz bN) => az bz. suff aux: quasi_bij BZopp I J. rewrite (csum_Cn2 _ aux); rewrite /csumb; congr csum; apply: Lg_exten. by move => i /Iz iz; rewrite /opp_seq; bw. split. - move => i /(ZN_intP mz bN aN) [qa qb]; apply/(ZN_intP nz aN bN). split. by move: (zle_opp qb); rewrite (BZoppD mz az) (BZopp_K nz). move: (zle_opp qa); rewrite (BZoppD mz (ZSo bz)). by rewrite (BZopp_K nz) (BZopp_K bz). - by move => i j /Iz iz /Iz jz; move/(BZopp_inj iz jz). - move => i /(ZN_intP nz aN bN) [qa qb]. move:(proj32 qa) => iz; move:(BZopp_K iz) => mmi. exists (BZopp i) => //. apply/(ZN_intP mz bN aN); split. by rewrite /BZdiff - (BZoppD nz bz); apply: zle_opp. by rewrite - (BZopp_K az) - (BZoppD nz (ZSo az)); apply: zle_opp. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)