proposition: Lemma opp_seq_p5 A B k : fin_disj_fam A -> fin_disj_fam B -> Exercise6_32_conc A B k -> natp k -> Exercise6_32_conc (opp_seq A) (opp_seq B) k.
proof: Proof. move => [qa qb qc qd][eara rb rc rd][f [bf ha hb]] kN. move:(ZNz kN) => kz. exists f; split. have ->: (unionb (opp_seq A)) = unionb A. set_extens t => /setUb_P [y ya yb]; apply/setUb_P. move: ya yb; rewrite /opp_seq; aw => yz; rewrite(LgV yz) qb. exists (BZopp y) => //; exact: (ZSo yz). rewrite qb in ya;move:(ZSo ya) => yc; rewrite /opp_seq; aw. by exists (BZopp y) => //; bw => //; rewrite (BZopp_K ya). have -> //: (unionb (opp_seq B)) = unionb B. set_extens t => /setUb_P [y ya yb]; apply/setUb_P. move: ya yb; rewrite /opp_seq; aw => yz; rewrite(LgV yz) rb. exists (BZopp y) => //; exact: (ZSo yz). rewrite rb in ya;move:(ZSo ya) => yc; rewrite /opp_seq; aw. by exists (BZopp y) => //; bw => //; rewrite (BZopp_K ya). - move => i x iz; rewrite /opp_seq; bw => // xi. move:(ZSo iz) => oiz. move:(ha _ _ oiz xi) => [j /(ZN_intP oiz kN kN) [ja jb] jc]. move: (proj31 jb) => jz; move:(ZSo jz) => njz. exists (BZopp j); last by bw => //; rewrite (BZopp_K jz). apply/(ZN_intP iz kN kN); split. by move:(zle_opp jb); rewrite (BZoppD oiz kz) (BZopp_K iz). by move:(zle_opp ja); rewrite (BZoppD oiz (ZSo kz))(BZopp_K iz)(BZopp_K kz). - move => i x iz; rewrite /opp_seq; bw => // xi. move:(ZSo iz) => oiz. move:(hb _ _ oiz xi) => [j /(ZN_intP oiz kN kN) [ja jb] jc]. move: (proj31 jb) => jz; move:(ZSo jz) => njz. exists (BZopp j); last by bw => //; rewrite (BZopp_K jz). apply/(ZN_intP iz kN kN); split. by move:(zle_opp jb); rewrite (BZoppD oiz kz) (BZopp_K iz). by move:(zle_opp ja); rewrite (BZoppD oiz (ZSo kz))(BZopp_K iz)(BZopp_K kz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)