~/jendhub

law le_double

bend-mathlib@0.8.1.0 · nat.bend:3610

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

3610# A natural is at most its double: n <= double n.
3611law le_double:
3612  for n: Nat
3613  le(n, Nat.double(n))

Uses (7)

Used by (0)

No other definition uses this definition.