Lemma app_non_empty : forall (A : Type) (xs : list A) (y : A),
  xs ++ [y] <> [].
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
