Proving algorithm for removing nodes from a complete graph with two kinds of edges Lets say $G$ is complete undirected graph with a set of edges coloured either black or red. The problem is to find an algorithm answering if it is possible to remove a subset of nodes from $G$ in a way such that all black edges are gone, but for any two nodes in the set of removed nodes there was no red edge between them.

I think I found a solution: If the graph has more than one black strongly connected components, then the answer is "no", because then there are two black edges $E_1$ and $E_2$ with no common nodes, and for every black edge at least one of its nodes should be removed to remove that edge from graph, and for any pair of nodes of $E_1$ and $E_2$ we choose to remove, there is a red edge between them, so we fail. Otherwise, we can sort all nodes by the number of linked black edges in descending order and then iterate this list node by node removing them from graph. If for current node there is a linked red edge, then mark the node on other end as "dangerous", and if we come across such node before all black edges are gone, then answer is "no". Otherwise, when there is no black edges, stop and answer "yes".

But now I want to prove this algorithm is correct. I think the case of more than one black SCCs is simple and doesn't require anything more rigorous, but the other case is more complicated and I'm not even entirely sure it's correct. Currently this is where I got:

Lets say the strategy of always removing a node with more linked black edges first is incorrect. Then it means, such strategy can make algorithm answer "no" when there was an other way to choose nodes which would make algorithm answer "yes". Then there is a step where some max-black-edges node $X$ is improperly chosen. Lets take a look at set of its black-adjacent nodes $S$. If all of them have the same number of linked black edges as $X$, then all other choices are symmetric and we will fail anyway, otherwise, there are nodes with less linked black edges than $X$ which means there are at least two nodes in $S$ which have a red edge between them. And to remove all black edges that make nodes in $S$ black-adjacent to $X$, we should remove all these nodes, so we will remove two with that red edge, so such strategies are incorrect and max-black-edges nodes should always be removed first.

I think this proof is somewhat naive and vague (especially in the end) and maybe even incorrect, so I'm seeking suggestions to make a better one. Not necessarily super-formal, but at least something which is sufficiently strict and believable.
A complete graph with red and black edges is just an unnecessarily complicated way of describing an arbitrary graph (where black edges correspond to neighbors and red edges to non-neighbors).

Effectively, given a graph $G$ you are looking for a subset of the vertices that is both a clique and a vertex cover.

Restating the problem like this, it is easier to see that your arguments are correct: in a graph with no isolated vertices, if there is more than one connected component (in an undirected graph every connected component is also strongly connected so stating "strongly connected" is redundant) then clearly there is no clique that covers both components.

Let $\Delta$ be the maximum degree of the graph $G=(V,E)$ and let $v$ be a degree-$\Delta$ vertex. Suppose there is a valid solution $S\subseteq V$ that does not contain $v$, then this solution must contain all of $v$'s neighbors. Suppose $S$ can not be extended to a valid solution by adding $v$, then $S$ contains some vertex not adjacent to $v$, thus the graph restricted to $S$ is a clique of size least $\Delta+1$ in which all vertices have degree at least $\Delta$. However, then the graph restricted to $S\cup{v}$ has a vertex of degree at least $\Delta+1$, contradicting that $\Delta$ is the maximum degree. Thus if a valid solution exists then this solution remains valid when adding a maximum-degree vertex.

So the algorithm can be restated in much simpler terms: take all maximum-degree vertices, and check that they are a valid solution.