proposition: Lemma err_aux: forall x y e1 e2, err x y e1 -> e1 <= e2 -> err x y e2.
proof: Proof. intros x y e1 e2 H1 H2. apply Rle_trans with (e1*Rabs y). exact H1. apply Rmult_le_compat_r. apply Rabs_pos. exact H2. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)