proposition: Lemma shiftl_mult_l x y n : x * (y ≪ n) = (x * y) ≪ n.
proof: Proof. pattern n. apply biinduction; clear n. solve_proper. now rewrite ?shiftl_0. intros m. rewrite ?shiftl_S. split; intros E. rewrite <-E. ring. apply (left_cancellation (.*.) 2). rewrite <-E. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders