def le_cancel_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:828

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

828def le_cancel_r(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == Nat.is_le(a, b) : Bool}:
829  Equal.cong(Cmp, Bool, t => Cmp.is_le(t), Nat.cmp(Nat.add(a, c), Nat.add(b, c)), Nat.cmp(a, b), NC.cmp_addr(a, b, c))