proposition: Fact composed_permutation_extends n f g : (forall i, i < n -> f i = g i) -> g n = n -> composed_permutation n f -> composed_permutation (S n) g.
proof: Proof. intros H1 H2 H3; revert H3 g H1 H2. induction 1 as [ f Hg | f i j p q H1 H2 IH2 H3 ]; intros g H4 H5. + constructor 1; intros j Hj. destruct (eq_nat_dec j n); subst; auto. rewrite <- H4, Hg; auto; lia. + constructor 2 with i j (flat n p) (flat n q). * destruct H1 as [ G1 G2 G3 G4 G5 ]; constructor; try lia. - rewrite flat_left; auto; lia. - rewrite flat_left; auto; lia. - intros k ? ? ?. destruct (eq_nat_dec k n); subst. ++ rewrite flat_right; auto. ++ rewrite flat_left, G5; lia. * apply IH2. - intros l Hl; rewrite flat_left; auto. - rewrite flat_right; lia. * intros k Hk. destruct (eq_nat_dec k n); subst. - rewrite (flat_right p), flat_right; lia. - rewrite (flat_left p); try lia. rewrite flat_left, <- H4; try lia. ++ apply H3; lia. ++ destruct H1 as [ G1 G2 G3 G4 G5 ]. destruct (eq_nat_dec k i). { subst; auto. } destruct (eq_nat_dec k j). { subst k; lia. } rewrite G5; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)