proposition: Lemma abeLeab: (Rabs b <= Rabs a)%R -> (2*powerRZ radix (Fexp b) <= Rabs (a+b))%R -> (Rabs (a+b) <= Rabs (a+b+e) *4/3)%R.
proof: Proof. intros. assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac]. assert (0 <4)%R; [apply Rlt_trans with 3%R; auto with real|idtac]. apply Rmult_le_reg_l with (3/4)%R; auto with real. unfold Rdiv; apply Rmult_lt_0_compat; auto with real. apply Rle_trans with (Rabs (a + b + e));[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (/4*Rabs (a + b))%R. apply Rle_trans with (Rabs (a+b));[right; field; auto with real|idtac]. pattern (a+b)%R at 1; replace (a+b)%R with ((a+b+e)+(-e))%R;[idtac|ring]. apply Rle_trans with (Rabs (a+b+e)+ Rabs (-e))%R;[apply Rabs_triang|idtac]. rewrite Rplus_comm; apply Rplus_le_compat_r. rewrite Rabs_Ropp; apply Rle_trans with (1:=eLeb). apply Rmult_le_reg_l with 4%R; auto with real. apply Rle_trans with (Rabs (a+b));[idtac|right; field; auto with real]. apply Rle_trans with (2:=H0). unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith. right; field; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz