proposition: Lemma shiftl_spec_from_int_pow `{SemiRing A} `{!PropHolds ((2:A) ≠ 0)} `{SemiRing B} `{!IntPowSpec A B ip} (sl : ShiftL A B) : (∀ x n, x ≪ n = x * 2 ^ n) → ShiftLSpec A B sl.
proof: Proof. pose proof int_pow_proper. intros spec. split. intros ? ? E1 ? ? E2. rewrite 2!spec. now rewrite E1, E2. intro x. rewrite spec, int_pow_0. now apply right_identity. intros x n. rewrite 2!spec. rewrite int_pow_S by solve_propholds. now rewrite ?associativity, (commutativity x 2). Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra