proposition: Theorem FmultRadixInv : forall (x z : float) (y : R), Fbounded b x -> Closest b radix y z -> (/ 2 * x < y)%R -> (/ 2 * x <= z)%R.
proof: Proof. intros x z y H' H'0 H'1. case MinEx with (r := (/ 2 * x)%R) (3 := pGivesBound); auto with zarith. intros min isMin. case MaxEx with (r := (/ 2 * x)%R) (3 := pGivesBound); auto with zarith. intros max isMax. case (Rle_or_lt y max); intros Rl1. case Rl1; clear Rl1; intros Rl1. replace (FtoRradix z) with (FtoRradix max). apply isMax_inv1 with (1 := isMax). apply sym_eq. unfold FtoRradix in |- *; apply ClosestMaxEq with (b := b) (r := y) (min := min); auto. apply isMinComp with (r1 := (/ 2 * x)%R) (max := max); auto. apply Rle_lt_trans with (2 := H'1); auto. apply isMin_inv1 with (1 := isMin). apply isMaxComp with (r1 := (/ 2 * x)%R) (min := min); auto. apply Rle_lt_trans with (2 := H'1); auto. apply isMin_inv1 with (1 := isMin). replace (FtoR radix min + FtoR radix max)%R with (FtoRradix x). apply Rmult_lt_reg_l with (r := (/ 2)%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; try rewrite Rmult_1_l; auto with real. unfold FtoRradix in |- *; apply (div2IsBetween b radix precision); auto. cut (Closest b radix max z); [ intros C0 | idtac ]. replace (FtoRradix z) with (FtoRradix max); auto. rewrite <- Rl1; auto. apply Rlt_le; auto. apply ClosestIdem; auto. case isMax; auto. apply (ClosestCompatible b radix y max z z); auto. case H'0; auto. apply Rle_trans with (FtoRradix max); auto. apply isMax_inv1 with (1 := isMax). apply (ClosestMonotone b radix (FtoRradix max) y); auto. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. case isMax; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz