Definition divisible8 (x : nat) : Prop :=
  modulo x 8 = 0.
