proposition: Theorem RND_Min_Pos_monotone : forall r s : R, (0 <= r)%R -> (r <= s)%R -> (RND_Min_Pos r <= RND_Min_Pos s)%R.
proof: Proof. intros r s V1 H. cut (0 <= s)%R; [ intros V2 | apply Rle_trans with (1 := V1); auto with real ]. rewrite <- FPredSuc with (x := RND_Min_Pos s) (precision := p) (b := b) (radix := radix); auto with zarith. 2: apply RND_Min_Pos_canonic; auto. unfold FtoRradix in |- *; apply FPredProp; auto with zarith; fold FtoRradix in |- *. apply RND_Min_Pos_canonic; auto. apply FSuccCanonic; auto with zarith; apply RND_Min_Pos_canonic; auto. apply Rle_lt_trans with r; auto with real. apply RND_Min_Pos_Rle; auto. apply Rle_lt_trans with (1 := H). replace (FtoRradix (FSucc b radix p (RND_Min_Pos s))) with (RND_Min_Pos s + powerRZ radix (Fexp (RND_Min_Pos s)))%R. unfold RND_Min_Pos in |- *; case (Rle_dec (firstNormalPos radix b p) s); intros H1. unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rle_lt_trans with ((s * powerRZ radix (- IRNDD (ln s / ln radix + (- Z.pred p)%Z)) - 1) * powerRZ radix (IRNDD (ln s / ln radix + (- Z.pred p)%Z)) + powerRZ radix (IRNDD (ln s / ln radix + (- Z.pred p)%Z)))%R; auto with real. right; ring_simplify. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with zarith real. ring_simplify (-IRNDD (ln s / ln radix + (- Z.pred p)%Z) + IRNDD (ln s / ln radix + (- Z.pred p)%Z))%Z; simpl; ring. apply Rplus_lt_compat_r; apply Rmult_lt_compat_r. apply powerRZ_lt, IZR_lt; lia. apply IRNDD_correct3. unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rle_lt_trans with ((s * powerRZ radix (dExp b) - 1) * powerRZ radix (- dExp b) + powerRZ radix (- dExp b))%R; auto with real. right; ring_simplify. rewrite Rmult_assoc; rewrite <- powerRZ_add; try apply IZR_neq; auto with zarith real. ring_simplify (dExp b + -dExp b)%Z; simpl in |- *; ring. apply Rplus_lt_compat_r; apply Rmult_lt_compat_r. apply powerRZ_lt, IZR_lt; lia. apply IRNDD_correct3. replace (powerRZ radix (Fexp (RND_Min_Pos s))) with (FtoR radix (Float 1 (Fexp (RND_Min_Pos s)))); [ idtac | unfold FtoR in |- *; simpl in |- *; ring ]. rewrite <- FSuccDiff1 with b radix p (RND_Min_Pos s); auto with zarith. rewrite Fminus_correct; auto with zarith; fold FtoRradix in |- *; ring. cut (- nNormMin radix p < Fnum (RND_Min_Pos s))%Z; auto with zarith. apply Z.lt_le_trans with 0%Z. replace 0%Z with (- (0))%Z; unfold nNormMin in |- *; auto with arith zarith. apply Zlt_Zopp, Zpower_nat_less; lia. apply le_IZR; unfold RND_Min_Pos in |- *; case (Rle_dec (firstNormalPos radix b p) s); intros H1; simpl in |- *; apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply powerRZ_le, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz