Theorem compatVersionChangeMaxAssoc : forall x y z,
  compatVersionChangeMax x (compatVersionChangeMax y z) = compatVersionChangeMax (compatVersionChangeMax x y) z.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.
