proposition: Lemma preserves_shiftl_exp x (n : B1) : x ≪ f n = x ≪ n.
proof: Proof. revert n. apply biinduction. solve_proper. now rewrite rings.preserves_0, ?shiftl_0. intros n. rewrite rings.preserves_plus, rings.preserves_1, ?shiftl_S. split; intros E. now rewrite E. now apply (left_cancellation (.*.) 2). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders