proposition: Lemma change_rel_aux: forall x y b, (0 <= b /\ Rabs (x - y) <= b * Rabs y)%R <-> (exists eps, -b <= eps <= b /\ x = y * (1 + eps))%R.
proof: Proof. intros x y b. split. intros (H1, H2). destruct (Req_dec y 0) as [Hy|Hy]. exists 0%R. repeat split. rewrite <- Ropp_0. now apply Ropp_le_contravar. apply H1. rewrite Hy, Rmult_0_l. destruct (Req_dec x 0) as [Hx|Hx] ; try exact Hx. elim Rabs_no_R0 with (1 := Hx). apply Rle_antisym. now rewrite Hy, Rminus_0_r, Rabs_R0, Rmult_0_r in H2. apply Rabs_pos. exists ((x - y) / y)%R. split. 2: now field. apply Rabs_def2b. apply Rmult_le_reg_l with (Rabs y). now apply Rabs_pos_lt. rewrite <- Rabs_mult. replace (y * ((x - y) / y))%R with (x - y)%R by now field. now rewrite Rmult_comm. intros (eps, (H1, H2)). repeat split. destruct (Rle_or_lt 0 b) as [H|H] ; try exact H. apply Ropp_le_cancel. apply Rle_trans with b. now apply Rle_trans with eps. apply Rlt_le. now rewrite Ropp_0. rewrite H2. replace (y * (1 + eps) - y)%R with (eps * y)%R by ring. rewrite Rabs_mult. apply Rmult_le_compat_r. apply Rabs_pos. unfold Rabs. destruct (Rcase_abs eps) as [H|H]. apply Ropp_le_cancel. now rewrite Ropp_involutive. apply H1. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library