proposition: Lemma not_cp_min_cp_max : forall a b, ~cp_min a b = b->cp_max a b = b.
proof: Proof. intros [a | | ][b | | ]; simpl; try (intuition; fail). destruct (Zle_or_lt a b). rewrite Z.max_comm; rewrite Zle_to_Zmax; auto. rewrite Z.min_comm; rewrite Zle_to_Zmin; auto with zarith. intros Hn; elim Hn; auto. Qed.
imports: ZArith List Lia