proposition: Theorem round_unique : forall rnd : R -> R -> Prop, round_pred_monotone rnd -> forall x f1 f2, rnd x f1 -> rnd x f2 -> f1 = f2.
proof: Proof. intros rnd Hr x f1 f2 H1 H2. apply Rle_antisym. now apply Hr with (3 := Rle_refl x). now apply Hr with (3 := Rle_refl x). Qed.
imports: Coq(Reals) Raux Defs