proposition: Lemma Rreal_int : {subset int_num <= Rreal}.
proof: Proof. exact: rpred_int_num. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)