proposition: Theorem IRNDD_eq : forall (r : R) (z : Z), (z <= r)%R -> (r < Z.succ z)%R -> IRNDD r = z.
proof: Proof. intros r z H1 H2. cut (IRNDD r - z < 1)%Z; [ intros H3 | apply lt_IZR; rewrite <- Z_R_minus; simpl in |- * ]. cut (z - IRNDD r < 1)%Z; [ intros H4; auto with zarith | apply lt_IZR; rewrite <- Z_R_minus; simpl in |- * ]. unfold Rminus in |- *; apply Rle_lt_trans with (r + - IRNDD r)%R; auto with real. apply Rlt_le_trans with (r + - (r - 1))%R; auto with real. 2: right; ring. apply Rplus_lt_compat_l, Ropp_lt_contravar. apply IRNDD_correct3. unfold Rminus in |- *; apply Rle_lt_trans with (r + - z)%R; auto with real. apply Rplus_le_compat_r; apply IRNDD_correct1. apply Rlt_le_trans with (Z.succ z + - z)%R; auto with real; right; unfold Z.succ in |- *; rewrite plus_IZR; simpl in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz