proposition: Lemma preserves_shiftl x (n : B) : f (x ≪ n) = (f x) ≪ n.
proof: Proof. revert n. apply biinduction. solve_proper. now rewrite 2!shiftl_0. intros n; split; intros IH. rewrite 2!shiftl_S. now rewrite rings.preserves_mult, rings.preserves_2, IH. apply (left_cancellation (.*.) 2). rewrite <-(rings.preserves_2 (f:=f)) at 1. rewrite <-rings.preserves_mult, <-shiftl_S, IH. now rewrite shiftl_S. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders