~/jendhub

law odd_lt_double

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

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

145law odd_lt_double:
146  for a: Nat
147  for b: Nat
148  for h: MNat.lt(a, b)
149  MNat.lt(1n+Nat.double(a), Nat.double(b))

Uses (5)

Used by (1)