proposition: Lemma AbsIR_mult : forall (x c: IR) (H : [0] [<=]c), c[*] AbsIR (x) [=] AbsIR (c[*]x).
proof: Proof. intros. unfold AbsIR. simpl. unfold ABSIR. rstepr (Max (c[*]x) (c[*]([--]x))). apply eq_symmetric_unfolded. apply max_mult; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq