def eq_cancel_r

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

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

724def eq_cancel_r(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_eq(Nat.add(a, c), Nat.add(b, c)) == Nat.is_eq(a, b) : Bool}:
725  Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(Nat.add(a, c), Nat.add(b, c)), Nat.cmp(a, b), NC.cmp_addr(a, b, c))