law double_ne_succ_double

bend-mathlib@0.8.1.0 · nat.bend:3812

import Base

3812# An even number is not odd: double a differs from 1 + double b.
3813law double_ne_succ_double:
3814  for a: Nat
3815  for b: Nat
3816  {Nat.double(a) != 1n+Nat.double(b) : Nat}