proposition: Lemma shiftl_base_plus x y n : (x + y) ≪ n = x ≪ n + 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