proposition: Fact decomp_lr_spec n : S n = power (decomp_l n) 2 * (2 * (decomp_r n) + 1).
proof: Proof. apply (proj2_sig (projT2 (@decomp_recomp_full (S n) (Nat.neq_succ_0 _)))). Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat gcd sums pos vec)