proposition: Lemma Qabs_5: forall q p, Qabs q <= p -> (- p <= q)/\ (q<= p).
proof: Proof. intros [|q|q] [|p|p]; simpl; unfold Qle; intros Hqp; split; auto; solve [ apply Zero_not_lt_Qneg|apply Qpos_not_lt_Qneg|apply Qle_opp; simpl; assumption]. Qed.