law le_ne

lawful-words@0.1.0.0 · proof_nat.bend:1500

import Base

1500# a <= b and a != b give a + 1 <= b.
1501law le_ne:
1502  for +a: Nat
1503  for +b: Nat
1504  for +le: {Nat.is_le(a, b) == True{} : Bool}
1505  for +ne: {Nat.is_eq(a, b) == False{} : Bool}
1506  {Nat.is_le(1n+a, b) == True{} : Bool}