proposition: Lemma rel_helper : forall xa xe b : R, xe <> 0 -> (Rabs ((xa - xe) / xe) <= b <-> Rabs (xa - xe) <= b * Rabs xe).
proof: Proof. intros xa xe b Zx. unfold Rdiv. rewrite Rabs_mult, Rabs_Rinv by exact Zx. split ; intros H. - apply Rmult_le_reg_r with (/ Rabs xe). apply Rinv_0_lt_compat. now apply Rabs_pos_lt. rewrite Rmult_assoc, Rinv_r, Rmult_1_r. exact H. now apply Rabs_no_R0. - apply Rmult_le_reg_r with (Rabs xe). now apply Rabs_pos_lt. rewrite Rmult_assoc, Rinv_l, Rmult_1_r. exact H. now apply Rabs_no_R0. Qed.
imports: Coq(Reals) Flocq(Core) Gappa(Gappa_tactic) Interval(Tactic)