Function law_add_nonnegative_saturating_never_decreases_left_operand 

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