proposition: Lemma shiftl_base_nat_pow `{Naturals B2} `{!NatPowSpec A B2 pw} `{!SemiRing_Morphism (f : B2 → B)} x n m : (x ≪ n) ^ m = (x ^ m) ≪ (n * f m).
proof: Proof. revert m. apply naturals.induction. solve_proper. rewrite ?nat_pow_0. now rewrite rings.preserves_0, rings.mult_0_r, shiftl_0. intros m E. rewrite rings.preserves_plus, rings.preserves_1. rewrite rings.plus_mult_distr_l, rings.mult_1_r, shiftl_exp_plus. rewrite !nat_pow_S, E. now rewrite shiftl_mult_l, shiftl_mult_r. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders