proposition: Lemma shiftl_2 x : x ≪ (2:B) = 4 * x.
proof: Proof. rewrite shiftl_S, shiftl_1. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders