Description: Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014) (Revised by Mario Carneiro, 30-Apr-2015)