proposition: Lemma Qcinv_neg : forall q, /q < 0 <-> q < 0.
proof: Proof. intro q; split; intro Hlt; apply Qcopp_lt_compat in Hlt; setoid_rewrite <- Qcopp_involutive at 1 2; apply Qcopp_lt_compat; replace (- 0) with 0 in * by ring; now rewrite <- Qcinv_opp_comm, Qcinv_pos in *. Qed.
imports: Qfield Qreduction Qcanon