proposition: Lemma FAbs_nonneg : forall F x Hx, [0] [<=] FAbs F x Hx.
proof: Proof. intros. 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