proposition: Lemma BQopp_fb: bijection (Lf BQopp BQ BQ).
proof: Proof. apply: lf_bijective. - by move => t tz; apply: QSo. - apply: BQopp_inj. - by move => y yz; move: (QSo yz)=> yz'; exists (BQopp y) => //;rewrite BQopp_K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)