proposition: Fact ra_decomp_r_rel n : { b | ⟦ra_decomp_r⟧ (n##vec_nil) b /\ exists a, ⟦ra_decomp_l⟧ (n##vec_nil) a /\ S n = power a 2 * (2*b+1) }.
proof: Proof. destruct (ra_decomp_l_rel n) as (a & H1 & H2 & H3). exists (div (S n) (power (S a) 2)); split. + exists (S n##power (S a) 2##vec_nil); split. { apply ra_div_val; generalize (@power_ge_1 (S a) 2); intros; lia. } pos split; simpl; auto. * exists (n##vec_nil); split; simpl; auto. pos split; simpl; auto. * exists (S a##vec_nil); split; auto. pos split; simpl; auto. exists (a##vec_nil); split; simpl; auto. pos split; simpl; auto. exists (n##vec_nil); split; auto. pos split; simpl; auto. + exists a; split; auto. generalize (div_rem_spec1 (S n) (power a 2)). apply divides_rem_eq in H2; rewrite H2, Nat.add_0_r. rewrite power_S in *. clear H1; revert H2 H3. generalize (S n) (power a 2) (power2_gt_0 a); clear n a; intros n p H1 H2 H3 H4. rewrite H4 at 1; rewrite Nat.mul_comm; f_equal. rewrite divides_rem_eq in H3. rewrite (Nat.mul_comm _ p), div_mult; try lia. rewrite Nat.mul_comm, rem_mult in H3; try lia. rewrite (@div_rem_spec1 (div n p) 2) at 1. rewrite H2 in H3; simpl in H3. generalize (@div_rem_spec2 (div n p) 2); intros H5. rewrite Nat.mul_comm in H3. destruct (rem (div n p) 2) as [ | [ | ] ]; 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)