proposition: Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.
proof: Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. now rewrite !Z.mul_opp_l, <- Z.opp_le_mono. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool