proposition: Fact ra_decomp_l_val n : ⟦ra_decomp_l⟧ (n##vec_nil) (decomp_l n).
proof: Proof. apply ra_decomp_lr_val. 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)