law le_ne

minebender-game@1.0.0.0 · proof_base.bend:540

import Base

540# a <= b and a != b give a + 1 <= b.
541law le_ne:
542  for +a: Nat
543  for +b: Nat
544  for le: {Nat.is_le(a, b) == True{} : Bool}
545  for ne: {Nat.is_eq(a, b) == False{} : Bool}
546  {Nat.is_le(1n+a, b) == True{} : Bool}