prove Lemma is_category_groupoid

Lemma is_category_groupoid (C : precategory) : is_groupoid C -> is_category C.