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