proposition: Lemma FAbs_char : forall x Hx Hx', FAbs x Hx [=] AbsIR (F x Hx').
proof: Proof. intros. simpl in |- *; unfold ABSIR in |- *; apply MAX_wd; algebra. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq