proposition: Lemma Qabs_Qminus_bound:forall low up q1 q2, low <= q1 -> q1 <= up -> low <= q2 -> q2 <= up -> Qabs (q1-q2) <= up-low.
proof: Proof. intros l u q1 q2 Hq1l Hq1u Hq2l Hq2u. destruct (Q_le_lt_dec q2 q1) as [H|H]; [ rewrite Qabs_eq; [ | apply Qle_Qminus_Zero ] | rewrite Qabs_non_eq_neg; [ stepl (q2-q1);[|ring] | apply Qlt_Qminus_Zero_neg ] ]; trivial; unfold Qminus; apply Qle_plus_plus; try apply Qopp_Qle; trivial. Qed.