proposition: Lemma FAbs_char' : forall F x Hx, AbsIR (FAbs F x Hx) [=] AbsIR (F x (ProjIR1 Hx)).
proof: Proof. intros. eapply eq_transitive_unfolded. apply AbsIR_eq_x. 2: apply FAbs_char. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply FAbs_char with (Hx' := ProjIR1 Hx). apply AbsIR_nonneg. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq