proposition: Fact ra_decomp_l_rel n : { a | ⟦ra_decomp_l⟧ (n##vec_nil) a /\ divides (power a 2) (S n) /\ ~ divides (power (S a) 2) (S n) }.
proof: Proof. exists (prim_min (fun i => notdiv_pow2 (S i) (S n)) (S n)); split. 1: { apply ra_decomp_l_val_0. } generalize (prim_min_spec (fun i => notdiv_pow2 (S i) (S n)) (S n)); intros (H1 & H2). 1: { apply notdiv_pow2_spec_2; intros C. apply divides_le in C; try discriminate. generalize (@power_ge_n (S (S n)) 2); intros; lia. } apply notdiv_pow2_spec_2 in H1; split; auto. revert H2; generalize (prim_min (fun i : nat => notdiv_pow2 (S i) (S n)) (S n)); intros [ | k ] Hk. + rewrite power_0; apply divides_1. + apply notdiv_pow2_spec_1, Hk; lia. 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)