proposition: Lemma shiftl_to_int_pow x n : f (x ≪ n) = f x * 2 ^ n.
proof: Proof. revert n. apply biinduction. solve_proper. now rewrite shiftl_0, int_pow_0, rings.mult_1_r. intros n. rewrite shiftl_S, int_pow_S by solve_propholds. rewrite rings.preserves_mult, rings.preserves_2. rewrite associativity, (commutativity (f x) 2), <-associativity. split; intros E. now rewrite E. now apply (left_cancellation (.*.) 2). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders