proposition: Lemma nat_of_pos_inj x y : nat_of_pos x = nat_of_pos y -> x = y.
proof: Proof. rewrite -!binnat.to_natE; apply Pos2Nat.inj. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)