proposition: Lemma nat_pow_3 x : x ^ (3:B) = x * (x * x).
proof: Proof. now rewrite nat_pow_S, nat_pow_2. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations