Commit 8841d22e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Moved Rmin_compare.

parent 71242001
......@@ -819,6 +819,20 @@ apply Rcompare_Gt.
now apply Rsqr_incrst_1.
Qed.
Theorem Rmin_compare :
forall x y,
Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.
Proof.
intros x y.
unfold Rmin.
destruct (Rle_dec x y) as [[Hx|Hx]|Hx].
now rewrite Rcompare_Lt.
now rewrite Rcompare_Eq.
rewrite Rcompare_Gt.
easy.
now apply Rnot_le_lt.
Qed.
End Rcompare.
Section Rle_bool.
......@@ -914,6 +928,7 @@ apply refl_equal.
Qed.
End Req_bool.
Section Floor_Ceil.
(** Zfloor and Zceil *)
......
......@@ -1324,20 +1324,6 @@ apply Rlt_le.
now apply Znearest_N_strict.
Qed.
Theorem Rmin_compare :
forall x y,
Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.
Proof.
intros x y.
unfold Rmin.
destruct (Rle_dec x y) as [[Hx|Hx]|Hx].
now rewrite Rcompare_Lt.
now rewrite Rcompare_Eq.
rewrite Rcompare_Gt.
easy.
now apply Rnot_le_lt.
Qed.
Theorem generic_N_pt :
forall x,
Rnd_N_pt generic_format x (round rndN x).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment