law double_lt_double

bend-mathlib@0.8.1.0 · nat.bend:3635

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

import Base

3635# Doubling preserves the strict order: a < b implies double a < double b.
3636law double_lt_double:
3637  for a: Nat
3638  for b: Nat
3639  for h: lt(a, b)
3640  lt(Nat.double(a), Nat.double(b))

Uses (7)

Used by (3)