proposition: Lemma shiftl_negate_1_to_fourth x : f (x ≪ -2) = f x / 4.
proof: Proof. rewrite shiftl_to_int_pow. apply (left_cancellation (.*.) (2 * 2)). transitivity (f x * (2 * (2 * 2 ^ (-2)))); [ring |]. transitivity (f x * (4 / 4)); [| ring]. assert ((4:F) ≠ 0). setoid_replace 4 with (2*2) by ring. solve_propholds. rewrite dec_recip_inverse, <-!int_pow_S by assumption. setoid_replace (1 + (1 - 2) : Z) with (0 : Z) by ring. now rewrite 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