proposition: Lemma nat_pow_base_0 (n : B) : n ≠ 0 → 0 ^ n = 0.
proof: Proof. pattern n. apply naturals.induction; clear n. solve_proper. intros E. now destruct E. intros. rewrite nat_pow_S. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations