proposition: Fact injective_composed_permutation n f : bounded_injective n f -> composed_permutation n f.
proof: Proof. intros [ H1 H2 ]. revert f H1 H2; induction n as [ | n IHn ]; intros f H1 H2. + constructor 1; intros; lia. + destruct (find_max_fun n f) as (i & H3 & H4). destruct (le_lt_dec n (f i)) as [ C | C ]. - assert (f i = n) as Hf1. { apply Nat.le_antisymm; auto; apply le_S_n, H1; lia. } assert (forall j, j <= n -> j <> i -> f j < n) as Hf2. { intros j G1 G2. destruct (eq_nat_dec (f j) n). + contradict G2; apply H2; lia. + specialize (H1 j); lia. } specialize (IHn (fun x => f (swap i n x))). spec in IHn. { intros j Hj. destruct (eq_nat_dec j i). + subst j; rewrite swap_spec_i; apply Hf2; lia. + rewrite swap_spec; try lia; apply Hf2; lia. } spec in IHn. { intros u v G1 G2 G3. apply H2 in G3. + revert G3; apply swap_inj. + destruct (eq_nat_dec u i). - subst; rewrite swap_spec_i; lia. - rewrite swap_spec; lia. + destruct (eq_nat_dec v i). - subst; rewrite swap_spec_i; lia. - rewrite swap_spec; lia. } apply composed_permutation_S in IHn. 2: rewrite swap_spec_j, Hf1; auto. generalize (@swap_bounded_permut (S n) i n); intros G. do 2 (spec in G; try lia). constructor 2 with (1 := G) (2 := IHn). intros; rewrite swap_involutive; auto. - destruct (@php_fun n f) as (u & v & G1 & G2). { intros; apply Nat.le_lt_trans with (2 := C); auto. } apply H2 in G2; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)