proposition: Lemma shiftl_spec_from_nat_pow `{SemiRing A} `{SemiRing B} `{!NatPowSpec A B pw} (sl : ShiftL A B) : (∀ x n, x ≪ n = x * 2 ^ n) → ShiftLSpec A B sl.
proof: Proof. pose proof nat_pow_proper. intros spec. split. intros ? ? E1 ? ? E2. rewrite 2!spec. now rewrite E1, E2. intro x. rewrite spec, nat_pow_0. now apply right_identity. intros x n. rewrite 2!spec. rewrite nat_pow_S. now rewrite ?associativity, (commutativity x 2). Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra