proposition: Lemma shiftl_le_flip_l `{Negate B} `{!Ring B} (x y : A) (n : B) : x ≪ (-n) ≤ y ↔ x ≤ y ≪ n.
proof: Proof. now rewrite <-shiftl_le_flip_r, rings.negate_involutive. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders