proposition: Fact ra_decomp_l_val_0 n : ⟦ra_decomp_l⟧ (n##vec_nil) (prim_min (fun i => notdiv_pow2 (S i) (S n)) (S n)).
proof: Proof. exists (S n##S n##vec_nil); split. + apply ra_prim_min_val with (f := fun v i => notdiv_pow2 (S i) (vec_head v)). intros i v; vec split v with j; vec nil v. exists (S i##j##vec_nil); split; auto. pos split; simpl; auto. exists (i##vec_nil); split; simpl; auto. pos split; simpl; auto. + pos split; simpl; auto; exists (n##vec_nil); split; simpl; auto; 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)