def le_rw

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:51

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

51def le_rw(+a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +b: Nat, +b2: Nat, +hb: {b == b2 : Nat}, +h: {Nat.is_le(a2, b2) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
52  +h2 = L.subst(Nat, z => {Nat.is_le(z, b2) == True{} : Bool}, a2, a, Equal.sym(Nat, a, a2, ha), h)
53  L.subst(Nat, z => {Nat.is_le(a, z) == True{} : Bool}, b2, b, Equal.sym(Nat, b, b2, hb), h2)