proposition: Lemma Rabs_def1 : forall x y : CReal, x < y -> -x < y -> CReal_abs x < y.
proof: Proof. intros x y Hxlty Hmxlty. apply CRealLt_above in Hxlty. apply CRealLt_above in Hmxlty. destruct Hxlty as [i imaj]. destruct Hmxlty as [j jmaj]. specialize (imaj (Z.min i j) ltac:(lia)). specialize (jmaj (Z.min i j) ltac:(lia)). cbn in jmaj; unfold CReal_opp_seq in jmaj. exists (Z.min i j). unfold CReal_abs, CReal_abs_seq, CReal_abs_scale; rewrite CReal_red_seq. pose proof Qpower_0_lt 2 (Z.min i j)%Z ltac:(lra) as Hpowij. pose proof Qpower_le_compat_l 2 (Z.min i j)%Z i ltac:(lia) ltac:(lra) as Hpowlei. pose proof Qpower_le_compat_l 2 (Z.min i j)%Z j ltac:(lia) ltac:(lra) as Hpowlej. apply Qabs_case; intros Hcase; lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra