Add some missing corollary; suggest a different proof of some lemma