proposition: Lemma Rint_subring_closed : subring_closed Rint.
proof: Proof. split=> // _ _ /RintP[x ->] /RintP[y ->]; apply/RintP. by exists (x - y); rewrite rmorphB. by exists (x * y); rewrite rmorphM. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid