fact: Fixpoint project n : nat -> vec nat n := match n with | 0 => fun _ => vec_nil | S n => fun x => decomp_l x ## project _ (decomp_r x) end.
imports: Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat gcd sums pos vec)