proposition: Lemma opp_seq_p4 A B k : Exercise6_32_hyp A B k -> natp k -> Exercise6_32_hyp (opp_seq A) (opp_seq B) k.
proof: Proof. move => [qa qb qc qd] kN. have Ha i: intp i -> i +z ZN \0c = i by move => iz; rewrite BZsum_0r. have Hb i: intp i -> i -z ZN \0c = i by move => iz; rewrite BZdiff_0r. have kz := (ZNz kN). have aux A1 B1: Exercise6_32_in A1 B1 k -> Exercise6_32_in (opp_seq A1) (opp_seq B1) k. move => hc => n l nz lN lg1. move: (ZSo nz) (ZNz lN) => mz lz. rewrite (opp_seq_p3 _ nz NS0 lN). rewrite (opp_seq_p3 _ nz kN (NS_sum lN kN)). have ra: intp (BZopp n -z ZN l) by apply: (ZS_diff mz lz). move: (hc ((BZopp n) -z (ZN l)) l ra lN lg1). have ->: (ZN_int (BZopp n -z ZN l) \0c l) = (ZN_int (BZopp n) l \0c). by rewrite /ZN_int (Ha _ mz) (Hb _ ra) (BZsum_diff1 lz mz). have -> :(ZN_int (BZopp n -z ZN l) k (l +c k)) = (ZN_int (BZopp n) (l +c k) k). rewrite /ZN_int. rewrite - (BZsumA mz (ZSo lz) (ZNz (NS_sum lN kN))). rewrite - (BZsum_cN lN kN) (BZsumC (BZopp (ZN l))) -/(_ -z _). rewrite (BZdiff_sum lz kz) BZdiff_diff2 //. congr (_ <=c _); rewrite /csumb; apply: f_equal; apply: Lg_exten => //. move => i /(ZN_intP mz lN NS0) /proj1/proj32 iz; move: (ZSo iz) => miz. by rewrite /fdfc /opp_seq /fin_disj_fam_card;bw => //; rewrite (BZopp_K iz). move => i /(ZN_intP mz (NS_sum lN kN) kN) /proj1/proj32 iz. move: (ZSo iz) => miz. by rewrite /fdfc /opp_seq /fin_disj_fam_card;bw => //; rewrite (BZopp_K iz). move: (aux _ _ qc) (aux _ _ qd) => r1 r2. by move: (opp_seq_p1 qa)(opp_seq_p1 qb) => ra rb; split. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)