proposition: Lemma positive_of_posK : cancel positive_of_pos pos_of_positive.
proof: Proof. move=> n /=; rewrite /positive_of_pos /pos_of_positive /=. apply: val_inj; rewrite Nat2Pos.id ?insubdK -?topredE ?valP //. by apply/eqP; rewrite -lt0n valP. 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)