def un.le_double

bend-osdev-u32@0.1.0.0 · PROOF.bend:219

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

219def un.le_double(x: Nat) -> {Nat.is_le(x, Nat.double(x)) == True{} : Bool}:
220  match x:
221    case 0n:
222      {==}
223    case 1n+ +p:
224      un.le_trans(p, Nat.double(p), 1n+Nat.double(p), un.le_double(p), un.le_succ_self(Nat.double(p)))

Uses (6)

Used by (2)