~/jendhub

def un.le_dbl

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

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

160def un.le_dbl(x: Nat, y: Nat) -> {Nat.is_le(Nat.double(x), Nat.double(y)) == Nat.is_le(x, y) : Bool}:
161  match x y:
162    case 0n 0n:
163      {==}
164    case 0n 1n+q:
165      {==}
166    case 1n+p 0n:
167      {==}
168    case 1n+p 1n+q:
169      un.le_dbl(p, q)

Uses (4)

Used by (1)