proposition: Lemma cp_max_assoc : forall a b c, cp_max (cp_max a b) c = cp_max a (cp_max b c).
proof: Proof. intros [a | | ]; simpl; auto; intros [b | |]; simpl; auto; intros [c| |]; simpl; auto. rewrite Z.max_assoc; auto. Qed.
imports: ZArith List Lia