(x y : Words) : word_change_sign (x ++ y) = word_change_sign y ++ word_change_sign x. Proof. unfold word_change_sign. lhs nrapply (ap reverse). 1: nrapply list_map_app. nrapply reverse_app. Defined.
Require Import Basics Types Group Subgroup