fact: Definition int_to_nat (z : int) : nat := if z > 0 then `|z|%N else 0%N.
imports: HB(structures) ZArith mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements)