proposition: Fact power_0_inv p n : power p n = 0 <-> n = 0 /\ 0 < p.
proof: Proof. induction p as [ | p IHp ]. + rewrite power_0; lia. + rewrite power_S; split. * intros H. apply Nat.eq_mul_0 in H. rewrite IHp in H; lia. * intros (?&?); subst; simpl; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)