proposition: Lemma RtointK (x : R): x \is a Rint -> (Rtoint x)%:~R = x.
proof: Proof. move=> Ix; rewrite /Rtoint insubT /= [RHS](eqP (xchooseP (asboolP _ Ix))). by congr _%:~R; apply/eq_xchoose. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid