x : word_change_sign (word_change_sign x) = x. Proof. unfold word_change_sign. lhs_V nrapply list_map_reverse. lhs nrapply ap. 1: nrapply reverse_reverse. lhs_V nrapply list_map_compose. snrapply list_map_id. intros a ?. apply change_sign_inv. Defined.
Require Import Basics Types Group Subgroup