proposition: Fact composed_permutation_ext n f g : (forall i, i < n -> f i = g i) -> composed_permutation n f -> composed_permutation n g.
proof: Proof. intros H1 H2; revert H2 g H1. induction 1 as [ f Hg | f i j p q H1 H2 IH2 H3 ]; intros g H4. + constructor 1; intros; rewrite <- H4; auto. + constructor 2 with i j p q; auto. intros; rewrite <- H4; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)