proposition: Lemma opp_seq_p2 A: fin_disj_fam A -> opp_seq (opp_seq A) = A.
proof: Proof. move =>[qa qb qc qd]; rewrite/opp_seq; apply: fgraph_exten; aww. move => i iz; bw => //; [ by rewrite BZopp_K | by apply: ZSo]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)