proposition: Theorem AddExpGeUnderf: forall f1:float ,forall f2:float, forall g:float, forall e:Z, Closest bo radix (f1+f2) g -> (Fbounded bo f1) -> (Fbounded bo f2) -> (powerRZ radix e <= Rabs f1)%R -> (powerRZ radix e <= Rabs f2)%R -> ((FtoRradix g=0)%R \/ (powerRZ radix (e-precision+1) <= Rabs g)%R).
proof: Proof. intros. case (Req_dec g 0); auto; intros. right. elim plusExactExp with bo radix precision f1 f2 g; auto with zarith. intros s T; elim T; intros g' T'; elim T'; intros R1 T''; clear T T'. elim T''; intros R2 T; elim T; intros R3 T'; elim T'; intros R4 TT; clear T T' T''. elim TT; intros R5 T; elim T; intros R6 R7; clear T TT. replace (FtoRradix g) with (FtoRradix g'); auto with real. apply Rle_trans with (powerRZ radix (Fexp g')). apply Rle_powerRZ; auto with real zarith. apply Z.le_trans with (Z.min (Fexp f1) (Fexp f2)); auto with zarith. apply Zmin_Zle; apply FexpGeUnderf; auto. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl. apply Rle_trans with (1%Z*powerRZ radix (Fexp g'))%R; [simpl; right; ring |apply Rmult_le_compat_r; auto with real zarith]. apply powerRZ_le; try apply IZR_lt; auto with zarith. apply IZR_le. case (Zle_lt_or_eq 0 (Z.abs (Fnum g'))); auto with zarith real; intros. case (Z.eq_dec 0 (Fnum g')); intros. absurd (FtoR radix g=0)%R; auto with real. rewrite <- R3; unfold FtoR; simpl; rewrite <- e0; simpl; ring. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz