proposition: Lemma shiftl_order x n m: x ≪ n ≪ m = x ≪ m ≪ n.
proof: Proof. rewrite <-?shiftl_exp_plus. now rewrite commutativity. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders