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