proposition: Fact ra_project_val n p x : ⟦@ra_project n p⟧ (x##vec_nil) (vec_pos (@project n x) p).
proof: Proof. revert x; induction p as [ | n p IHp ]; intros x; simpl; auto. exists (decomp_r x##vec_nil); split. + apply IHp. + pos split; simpl; auto. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat gcd crt sums) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg recomp prim_min ra_utils)