proposition: Theorem AddExpGe1Underf2: 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 -> (-dExp bo <= e-1)%Z -> (FtoRradix g <>0)%R -> (powerRZ radix (e-precision) <= Rabs g)%R.
proof: Proof. intros. case (AddExpGe1Underf (Fnormalize radix bo precision f1) (Fnormalize radix bo precision f2) g e); auto. unfold FtoRradix; repeat rewrite FnormalizeCorrect; auto with real. apply FnormalizeCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. unfold FtoRradix; rewrite FnormalizeCorrect; auto with real. intros; absurd (FtoRradix g=0); auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz