proposition: Lemma BQopp_perm: inc (Lf BQopp BQ BQ) (permutations BQ).
proof: Proof. have h:= BQopp_fb; have h1:= (proj1 (proj1 h)). apply: Zo_i => //; apply/functionsP; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)