def double_self_le

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:426

import Base

426def double_self_le(+n: Nat) -> {Nat.is_le(n, Nat.double(n)) == True{} : Bool}:
427  match n:
428    case 0n:
429      {==}
430    case 1n+p:
431      le_trans(p, Nat.double(p), 1n+Nat.double(p), double_self_le(p), le_succ(Nat.double(p)))