proposition: Lemma BZopp_K x: intp x -> BZopp (BZopp x) = x.
proof: Proof. move => xz. move: C0_ne_C1 => ns. rewrite {1} /BZopp BZopp_val /BZopp; case: (equal_or_not(Q x) C0) => h; Ytac0. rewrite /BZ_of_nat/int_np; aw; Ytac0;apply:BZm_hi_pr. move/candu2P: xz => [px]; case; last by move => [_]; rewrite h. move => [pa pb];apply /setU1_P;left;apply /indexed_P;split => //. rewrite /BZm_of_nat /int_np; case: (equal_or_not (P x) \0c) => h1; Ytac0. by rewrite BZ0_sg; Ytac0; symmetry;apply: BZ_0_if_val0. aw;Ytac0; apply:BZp_hi_pr; move/candu2P: xz => [px]; case; first by move => [_]. by move => [pa pb]; apply /indexed_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)