def dle

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bl.bend:76

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

76def dle(+a: Nat, +c: Nat, +h: {Nat.is_le(Nat.double(a), Nat.double(c)) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
77  Equal.trans(Bool, Nat.is_le(a, c), Nat.is_le(Nat.double(a), Nat.double(c)), True{}, Equal.cong(Cmp, Bool, t => Cmp.is_le(t), Nat.cmp(a, c), Nat.cmp(Nat.double(a), Nat.double(c)), Equal.sym(Cmp, Nat.cmp(Nat.double(a), Nat.double(c)), Nat.cmp(a, c), NC.cmp_dbl(a, c))), h)