def internal_lt_congl

bend-mathlib@0.8.1.0 · u32.bend:264

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

264def internal_lt_congl(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: MNat.lt(x, m)) -> MNat.lt(y, m):
265  %e : MNat.lt(_, m)
266  h