proposition: Lemma BZopp_perm: inc (Lf BZopp BZ BZ) (permutations BZ).
proof: Proof. have h:= BZopp_fb; have h1:= (proj1 (proj1 h)). by apply: Zo_i => //; apply/functionsP; split => //; rewrite/BZopp_fun; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)