law double_sub

bend-mathlib@0.8.1.0 · nat.bend:3595

import Base

3595# Doubling distributes over truncated subtraction: double (a - b) = double a - double b.
3596law double_sub:
3597  for a: Nat
3598  for b: Nat
3599  {Nat.double(Nat.sub(a, b)) == Nat.sub(Nat.double(a), Nat.double(b)) : Nat}