Qclose_rounded@{} : Rounded Q. Proof. intros e q r;split. - intros E;apply Qclose_alt in E. pose proof (Q_average_between _ _ E) as [E1 E2]. apply tr;simple refine (exist _ (mkQpos ((abs (q - r) + ' e) / 2) _) _). { apply pos_mult_compat;[|solve_propholds]. red. apply pos_plus_le_lt_compat_r;[solve_propholds|apply Qabs_nonneg]. } simpl. exists (Qpos_diff _ _ E2). split. + apply pos_eq. exact (Qpos_diff_pr _ _ E2). + apply Qclose_alt. exact E1. - apply (Trunc_ind _). intros [d [d' [He xi]]]. apply Qclose_alt;rewrite He. apply Qclose_alt in xi. apply lt_le_trans with (' d);trivial. apply nonneg_plus_le_compat_r. solve_propholds. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.