proposition: Fact decomp_uniq a1 b1 a2 b2 : power a1 2 * (2*b1+1) = power a2 2 * (2*b2+1) -> a1 = a2 /\ b1 = b2.
proof: Proof. intros H. destruct (lt_eq_lt_dec a1 a2) as [ [ H1 | H1 ] | H1 ]. + exfalso; revert H; apply power_mult_lt_inj; auto. + split; auto; subst a2. rewrite Nat.mul_cancel_l in H; try lia. generalize (power2_gt_0 a1); lia. + exfalso; symmetry in H. revert H; apply power_mult_lt_inj; auto. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat gcd sums pos vec)