~/jendhub

law lt_of_double_lt

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

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

639law lt_of_double_lt:
640  for a: Nat
641  for b: Nat
642  for h: MNat.lt(Nat.double(a), Nat.double(b))
643  MNat.lt(a, b)

Uses (5)

Used by (1)