let pos_lemma = 
prove_by_refinement(
   `!Q. (?C. (&0 <= C /\  (!r. &1 <= r ==> Q r <= C * r pow 2))) <=> 
    (?C. (  (!r. &1 <= r ==> Q r <= C * r pow 2)))`,

[
GEN_TAC;
EQ_TAC;
REPEAT STRIP_TAC;
EXISTS_TAC `C:real`;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
EXISTS_TAC `abs(C)`;search[`negligible_fun_0`];;
REWRITE_TAC[REAL_ARITH `&0 <= abs C`];
REPEAT STRIP_TAC;
ASSUME_TAC (REAL_ARITH `C <= abs C`);
MATCH_MP_TAC REAL_LE_TRANS;
EXISTS_TAC `C * r pow 2`;
CONJ_TAC;
ASM_SIMP_TAC[];
MATCH_MP_TAC REAL_LE_RMUL_IMP;
ASM_REWRITE_TAC[Collect_geom.REAL_LE_POW_2];
]);;

let negligible_fun_any_C = 
prove(
   `!f S. negligible_fun_0 f S <=> 
    (?C.  (!r. &1 <= r ==> sum (S INTER ball ((vec 0),r)) f <= C * r pow 2))`,

  REWRITE_TAC[Pack_defs.negligible_fun_0;Pack_defs.negligible_fun_p;pos_lemma]);;