proposition: Theorem AddExpGeUnderf2: 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 (AddExpGeUnderf f1 f2 g e); auto. intros; absurd (FtoRradix g=0); auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz