Function rewrite_native_guarded_calls_expr 

pub fn rewrite_native_guarded_calls_expr(
    expr: &Spanned<Expr>,
    fn_name: &str,
    aux_name: &str,
) -> Spanned<Expr>

Walk expr and rewrite every recursive call to fn_name into a call to aux_name carrying an extra OMEGA_PROOF_SENTINEL ident at the end of the argument list. Used by the proof-mode IntCountdownGuarded lowering — the synthetic argument lets Lean discharge the precondition at every recursive site without touching the original Aver source.