proposition: Lemma shiftl_negate_1_to_half x : f (x ≪ -1) = f x / 2.
proof: Proof. rewrite shiftl_to_int_pow. apply (left_cancellation (.*.) 2). transitivity (f x * (2 * 2 ^ (-1))); [ring |]. transitivity (f x * (2 / 2)); [| ring]. rewrite dec_recip_inverse, <-int_pow_S by assumption. now rewrite rings.plus_negate_r, int_pow_0. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders