law lt_rw

bend-kit-lemmas@0.1.1.0 · lemmas.bend:408

import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas

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

408# Moves a strict upper bound across an equation without a conversion check.
409law lt_rw:
410  for -a: Nat
411  for -b: Nat
412  for -c: Nat
413  for e: {a == b : Nat}
414  for h: MNat.lt(b, c)
415  MNat.lt(a, c)

Uses (3)

Used by (5)