proposition: Fact pow2_dec_uniq p a q b : pow2 p*(2*a+1) = pow2 q*(2*b+1) -> p = q /\ a = b.
proof: Proof. revert q; induction p as [ | p IHp ]; intros [ | q ]. + simpl; lia. + rewrite pow2_fix0, pow2_fix1, <- Nat.mul_assoc; lia. + rewrite pow2_fix0, pow2_fix1, <- Nat.mul_assoc; lia. + rewrite !pow2_fix1, <- !Nat.mul_assoc; intros H. destruct (IHp q); lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)