proposition: Lemma pos_of_positiveK : cancel pos_of_positive positive_of_pos.
proof: Proof. move=> n /=; rewrite /positive_of_pos /pos_of_positive /=. by rewrite val_insubd to_nat_gt0 Pos2Nat.id. 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)