proposition: Lemma shiftl_le_flip_r `{Negate B} `{!Ring B} (x y : A) (n : B) : x ≤ y ≪ (-n) ↔ x ≪ n ≤ y.
proof: Proof. split; intros E. apply (order_reflecting (≪ -n)). now rewrite shiftl_reverse by now apply rings.plus_negate_r. apply (order_reflecting (≪ n)). now rewrite shiftl_reverse by now apply rings.plus_negate_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders