diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 192993212..0f436ec05 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -45,7 +45,7 @@ val impl__u128__pow: u128 -> u32 -> u128
 val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> (Math.Lemmas.pow2_lt_compat 15 (v exponent); result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent)))}
 val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}
 
-val impl__u8__count_ones: u8 -> u32
+val impl__u8__count_ones: u8 -> r:u32{v r <= 8}
 
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError