~/jendhub

def internal_le_congr

bend-mathlib@0.8.1.0 · u32.bend:268

import bend-mathlib@0.8.1.0/u32.bend as U32
import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

268def internal_le_congr(-m: Nat, -x: Nat, -y: Nat, e: {y == x : Nat}, h: MNat.le(m, y)) -> MNat.le(m, x):
269  %e : MNat.le(m, _)
270  h

Uses (2)

Used by (1)