proposition: Fact numq_div_lt0 n d : n != 0 -> d != 0 -> (numq (n%:~R / d%:~R) < 0)%R = (n < 0)%R (+) (d < 0)%R.
proof: Proof. move=> n0 d0; rewrite -sgr_cp0 sgr_numq_div !sgr_def n0 d0. by rewrite !mulr1n -signr_addb; case: (_ (+) _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)