proposition: Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y.
proof: Proof. split. - split. + rewrite <- (Qopp_opp x). apply Qopp_le_compat. apply Qle_trans with (Qabs (-x)). * apply Qle_Qabs. * now rewrite Qabs_opp. + apply Qle_trans with (Qabs x); auto using Qle_Qabs. - intros (H,H'). apply Qabs_case; trivial. intros. rewrite <- (Qopp_opp y). now apply Qopp_le_compat. Qed.
imports: QArith Qreduction