proposition: Fact project_inject n v : project _ (@inject n v) = v.
proof: Proof. induction v as [ | n x v IHv ]; simpl; auto. rewrite decomp_l_recomp, decomp_r_recomp; f_equal; trivial. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat gcd sums pos vec)