proposition: Lemma shiftl_negate `{Negate A} `{!Ring A} x n : (-x) ≪ n = -(x ≪ n).
proof: Proof. rewrite (rings.negate_mult x), (rings.negate_mult (x ≪ n)). symmetry. now apply shiftl_mult_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders