proposition: Theorem RND_Min_Pos_correct : forall r : R, (0 <= r)%R -> isMin b radix r (RND_Min_Pos r).
proof: Proof. intros r H1. split. apply FcanonicBound with radix; apply RND_Min_Pos_canonic; auto. split. apply RND_Min_Pos_Rle; auto. fold FtoRradix in |- *; intros f H2 H3. case (Rle_or_lt 0 f); intros H4. unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix b p f; auto; fold FtoRradix in |- *. rewrite <- RND_Min_Pos_projector. apply RND_Min_Pos_monotone; unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto. unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto. apply FnormalizeCanonic; auto with zarith. apply Rle_trans with 0%R; auto with real. unfold RND_Min_Pos in |- *; case (Rle_dec (firstNormalPos radix b p) r); intros H5; unfold FtoRradix, FtoR in |- *; simpl in |- *; apply Rmult_le_pos; auto with real zarith; try apply powerRZ_le, IZR_lt; try lia. apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz