def div2_double

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:522

import Base

522def div2_double(x: Nat) -> {Nat.div(Nat.double(x), 2n) == x : Nat}:
523  match x:
524    case 0n:
525      {==}
526    case 1n+ +y:
527      %double_succ(y) : {Nat.div(_, 2n) == 1n+y : Nat}
528      %Equal.sym(Nat, Nat.div(Nat.add(2n, Nat.double(y)), 2n), 1n+Nat.div(Nat.double(y), 2n), div2_step(Nat.double(y))) : {_ == 1n+y : Nat}
529      succ_cong(Nat.div(Nat.double(y), 2n), y, div2_double(y))