Commit 7773d1aa authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added reflexivity for Rnd_gNE.

parent e9dfd4d4
......@@ -159,14 +159,24 @@ apply Rnd_gNE_pt_unicity_prop.
Qed.
Theorem Rnd_gNE_pt_monotone :
forall x y f g : R,
Rnd_gNE_pt x f -> Rnd_gNE_pt y g ->
(x <= y)%R -> (f <= g)%R.
rounding_pred_monotone Rnd_gNE_pt.
Proof.
apply Rnd_NG_pt_monotone.
apply Rnd_gNE_pt_unicity_prop.
Qed.
Theorem Rnd_gNE_pt_refl :
forall x : R, format x ->
Rnd_gNE_pt x x.
Proof.
intros x Hx.
split.
now apply Rnd_N_pt_refl.
right.
intros f Hf.
now apply Rnd_N_pt_idempotent with format.
Qed.
Theorem Rnd_gNE_pt_idempotent :
forall x f : R,
Rnd_gNE_pt x f -> format 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