proposition: Lemma int_pow_4 x : x ^ (4:B) = x * (x * (x * x)).
proof: Proof. now rewrite int_pow_S_nonneg, int_pow_3 by solve_propholds. Qed.
imports: Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.nat_pow MathClasses.theory.int_abs MathClasses.theory.dec_fields