proposition: Lemma shiftl_1 x : x ≪ (1:B) = 2 * x.
proof: Proof. now rewrite <-(rings.plus_0_r 1), shiftl_S, shiftl_0. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders