proposition: Lemma shiftl_exp_plus x n m : x ≪ (n + m) = x ≪ n ≪ m.
proof: Proof. pattern m. apply biinduction; clear m. solve_proper. now rewrite shiftl_0, rings.plus_0_r. intros m. setoid_replace (n + (1 + m)) with (1 + (n + m)) by ring. rewrite ?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