fact: Definition BZ_le x y:= [/\ intp x, intp y & [\/ [/\ int_np x , int_np y & (BZ_val y) <=c (BZ_val x)], [/\ int_np x & int_pp y] | [/\ int_pp x, int_pp y & (BZ_val x) <=c (BZ_val y)]]].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)