proposition: Lemma err_mult_exact: forall x y e r, 0 < r -> err x y e -> err (/r*x) (/r*y) e.
proof: Proof. intros x y e r Hr H. assert (r <> 0). now apply Rgt_not_eq. apply Rmult_le_reg_l with r. exact Hr. rewrite <- (Rabs_right r) at 1 4. rewrite <- Rabs_mult. replace (r * (/ r * x - / r * y)) with (x-y) by now field. apply Rle_trans with (1:=H). rewrite (Rmult_comm (Rabs r) _), Rmult_assoc. rewrite <- Rabs_mult. replace (/r * y *r) with y by now field. apply Rle_refl. apply Rle_ge; now left. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)