proposition: Lemma shiftl_int_pow x n : x ≪ n = x * 2 ^ n.
proof: Proof. change (id (x ≪ n) = id x * 2 ^ n). apply shiftl_to_int_pow. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders