Lemma list_mod8_1 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)) -> divisible8 (length xs).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
