proposition: Lemma shiftl_mult_r x y n : (x ≪ n) * y = (x * y) ≪ n.
proof: Proof. now rewrite commutativity, shiftl_mult_l, commutativity. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders