proposition: Lemma seq_spec2 {d A B} : A ++ B ~p [0] ++ (map (fun i => (S d) + i) A) -> exists n, A ~p map (fun i => (S d) * i) (seq 0 n) /\ B = [(S d) * n].
proof: Proof. suff : forall k, A ++ B ~p [(1+d) * k] ++ (map (fun i => (1 + d) + i) A) -> A ~p map (fun i => (1+d) * i) (seq k (length A)) /\ B = [(1+d) * (k + length A)]. { have ->: [0] = [(1+d) * 0] by (congr cons; lia). move=> /[apply] ?. by exists (length A). } move=> k. elim /(Nat.measure_induction _ (@length nat)) : A k => A IH k H. move: (H) => /Permutation_length. rewrite ?app_length map_length /= => HAB. have [b Hb] : exists b, B = [b]. { move: (B) HAB => [|? [|? ?]] /=; [ by lia | by eexists | by lia ]. } subst B. move: (H) => /Permutation_sym /(Permutation_in ((1 + d) * k)) /(_ (in_eq _ _)) /in_app_iff []. - move /(@in_split nat) => [A1 [A2 ?]]. subst A. have := IH (A1 ++ A2). apply: unnest. { rewrite ?app_length /=. by lia. } move=> /(_ (1+k)). apply: unnest. { move: H. rewrite !map_app /= -!app_assoc /=. move=> /Permutation_sym /(@Permutation_cons_app_inv nat) <-. have -> : S (k + d * S k) = S (d + (k + d * k)) by lia. by apply /Permutation_sym /Permutation_middle. } move=> {IH} [IH ->]. constructor. + have ->: length (A1 ++ (1 + d) * k :: A2) = 1 + length (A1 ++ A2). { rewrite ?app_length /=. by lia. } rewrite /= -IH. by apply /Permutation_sym /Permutation_middle. + congr cons. rewrite !app_length /=. by lia. - case; last done. move=> ?. subst b. move: H => /Permutation_sym /(Permutation_cons_app_inv _ [] (A := nat)). rewrite app_nil_r. move=> /Permutation_map_lt_nil ->; first by lia. constructor=> /=; first done. congr cons. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun