(inv R (sum_field R (S N))
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
(lt_zero_to_le_inv_zero R (S N)
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
[ simplify;
(inv R (sum_field R (S N))
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
(lt_zero_to_le_inv_zero R (S N)
(not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
[ simplify;