proposition: Lemma RposI (p : pos) (x : positive) : refines Rpos p x -> x = positive_of_pos p.
proof: Proof. by move=> /RposE ->; rewrite pos_of_positiveK. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)