proposition: Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
proof: Proof. intros (x1,x2) (y1,y2); unfold Qle; simpl. rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.le_sub_le_add_r, Z.opp_involutive. reflexivity. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool