proposition: Lemma opp_seq_p6 A: supp_left_unbounded (fdfc A) -> ~supp_right_unbounded (fdfc A) -> ~ supp_left_unbounded (fdfc (opp_seq A)) /\ supp_right_unbounded (fdfc (opp_seq A)).
proof: Proof. move => ha hb; split. dneg h => i iz. move:(h _ (ZSo iz)) =>[j ja jb]; exists (BZopp j). by move:(zle_opp ja); rewrite (BZopp_K iz). move: (proj31 ja) => jz; move:(ZSo jz) => ojz. by move: jb; rewrite /opp_seq /fdfc /fin_disj_fam_card; bw. move => i iz. move:(ha _ (ZSo iz)) =>[j ja jb]; exists (BZopp j). by move:(zle_opp ja); rewrite (BZopp_K iz). move: (proj31 ja) => jz; move:(ZSo jz) => ojz. move: jb; rewrite /opp_seq /fdfc /fin_disj_fam_card; bw => //. by rewrite (BZopp_K jz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)