proposition: Lemma RintE n x : refines Rint n x -> n = int_of_Z x.
proof: Proof. by rewrite refinesE. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) CoqEAL(hrel param refinements) CoqEAL(pos binnat rational) tactics rat_of_Z