Function law_add_nonnegative_saturating_normalizes_negative_increment 

pub fn law_add_nonnegative_saturating_normalizes_negative_increment(
    x: i64,
    y: i64,
) -> bool