proposition: Fact composed_permutation_S n g : g n = n -> composed_permutation n g -> composed_permutation (S n) g.
proof: Proof. intro; apply composed_permutation_extends; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)