let
v_inf v1 v2 = v_larger_than_zero (v2 -~ v1)