proposition: Lemma BQ_sign_prop x: ratp x -> [/\ inc x BQps <-> BQsign x = \1z, inc x BQms <-> BQsign x = \1mz & x = \0q <-> BQsign x = \0z].
proof: Proof. move => xq. move: BZ1_nz BZm1_nz => n1 n2. have n3:(\1mz <> \1z). move:C1_ne_C0 => h. by rewrite /BZ_mone /BZm_of_nat (Y_false h) => /pr2_def /nesym. move:(@BQsign_pos x) (@BQsign_neg x) (BQsign_0) => pa pb pc. split; split => // h; case/BQ_i1P:xq => // xv. + by move: h; rewrite xv pc // => w; case n1. + by move: (pb xv); rewrite h => h1; case: n3. + by move:h; rewrite xv pc => h; case n2. + by move: (pa xv); rewrite h. + by rewrite h. + by rewrite h. + by rewrite h. + by move:(pa xv); rewrite h => w; case n1. + by move:(pb xv); rewrite h => w; case n2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)