proposition: Theorem php_fun : exists i j, i < j <= n /\ f i = f j.
proof: Proof. Proof using Hf. destruct PHP_rel with (R := fun x y => y = f x) (l := list_an 0 (S n)) (m := list_an 0 n) as (a & i & b & j & c & v & H1 & H2 & H3 & H4). + intros x; rewrite list_an_spec; simpl; intros [ _ H ]. exists (f x); split; auto; rewrite list_an_spec; simpl; split; try lia. apply Hf; lia. + do 2 rewrite list_an_length; auto. + exists i, j; split; try lia. generalize H1; intros G1. apply list_an_app_inv in G1. destruct G1 as (G0 & G1); simpl in G1. injection G1; clear G1; intros G1 G2. symmetry in G1; apply list_an_app_inv in G1. destruct G1 as (G3 & G1); simpl in G1. injection G1; clear G1; intros G4 G1. apply f_equal with (f := @length _) in H1. revert H1; rew length; intros H1. lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)