~/jendhub

law double_le_double

bend-mathlib@0.8.1.0 · nat.bend:3620

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

3620# Doubling preserves the order: a <= b implies double a <= double b.
3621law double_le_double:
3622  for a: Nat
3623  for b: Nat
3624  for h: le(a, b)
3625  le(Nat.double(a), Nat.double(b))

Uses (7)

Used by (1)