simplify proofs of powerdomain inequalities
move lemmas to Deflation.thy
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
add lemma finite_deflation_intro