proposition: Lemma shiftl_base_1_to_int_pow n : f (1 ≪ n) = 2 ^ n.
proof: Proof. now rewrite shiftl_to_int_pow, rings.preserves_1, rings.mult_1_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders