Commit 0e06838e by Guillaume Melquiond

### Renamed Z(floor/ceil)_Z to _Z2R.

parent fd490bb1
 ... ... @@ -333,7 +333,7 @@ apply Zfloor_lb. now apply Zfloor_lub. Qed. Theorem Zfloor_Z : Theorem Zfloor_Z2R : forall n, Zfloor (Z2R n) = n. Proof. ... ... @@ -392,13 +392,13 @@ rewrite opp_Z2R. now apply Ropp_lt_contravar. Qed. Theorem Zceil_Z : Theorem Zceil_Z2R : forall n, Zceil (Z2R n) = n. Proof. intros n. unfold Zceil. rewrite <- opp_Z2R, Zfloor_Z. rewrite <- opp_Z2R, Zfloor_Z2R. apply Zopp_involutive. Qed. ... ... @@ -431,8 +431,8 @@ Proof. intros n. unfold Ztrunc. destruct Rlt_le_dec as [H|H]. apply Zceil_Z. apply Zfloor_Z. apply Zceil_Z2R. apply Zfloor_Z2R. Qed. Theorem Ztrunc_floor : ... ... @@ -458,8 +458,8 @@ destruct Rlt_le_dec as [_|H]. easy. rewrite (Rle_antisym _ _ Hx H). fold (Z2R 0). rewrite Zceil_Z. apply Zfloor_Z. rewrite Zceil_Z2R. apply Zfloor_Z2R. Qed. Theorem Ztrunc_opp : ... ...
 ... ... @@ -35,7 +35,7 @@ Theorem canonic_mantissa_0 : Proof. unfold canonic_mantissa. rewrite Rmult_0_l. exact (Zfloor_Z 0). exact (Zfloor_Z2R 0). Qed. *) ... ... @@ -75,7 +75,7 @@ rewrite Ropp_mult_distr_l_reverse. rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r. rewrite Rmult_1_r. rewrite <- opp_Z2R. now rewrite 2!Zfloor_Z. now rewrite 2!Zfloor_Z2R. Qed. *) ... ... @@ -598,7 +598,7 @@ destruct (total_order_T 0 x) as [[Hx|Hx]|Hx]. now apply generic_DN_pt_pos. rewrite <- Hx, Rmult_0_l. fold (Z2R 0). rewrite Zfloor_Z, F2R_0. rewrite Zfloor_Z2R, F2R_0. apply Rnd_DN_pt_refl. apply generic_format_0. now apply generic_DN_pt_neg. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!