proposition: Theorem qGeUnderf: (a*c <> 0)%R -> (powerRZ radix (-dExp bo+3*precision-1) <= Rabs (q))%R.
proof: Proof. case U2; intros. absurd (a*c=0)%R; auto with real. assert (exists f:float, Fbounded bo f /\ (powerRZ radix (- dExp bo + 3 * precision - 1)= f)%R). exists (Float 1 (- dExp bo + 3 * precision - 1)). split;[split|unfold FtoRradix, FtoR; simpl; ring]. simpl; apply vNumbMoreThanOne with radix precision; auto with zarith. apply Z.le_trans with (- dExp bo + 3 * precision - 1)%Z; auto with zarith. elim H1; intros f T; elim T; intros; clear H1 T. rewrite H3; unfold FtoRradix. apply RoundAbsMonotonel with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. fold FtoRradix; rewrite <- H3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz