law le_step

lawful-bytes@0.1.1.0 · proof_same.bend:96

import Base

96# a + 1 + m <= b gives (a + 1) + m <= b.
97law le_step:
98  for +a: Nat
99  for +m: Nat
100  for +b: Nat
101  for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
102  {Nat.is_le(Nat.add(Nat.add(a, 1n), m), b) == True{} : Bool}