proposition: Lemma word_change_sign_inv x : word_change_sign (word_change_sign x) = x.
proof: Proof. induction x. 1: reflexivity. simpl. rewrite word_change_sign_ww. cbn; f_ap. apply change_sign_inv. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list