proposition: Lemma shiftl_negate_to_recip_nat_pow x n P2n : f (x ≪ (-g n)) = f x // (2 ^ n)↾P2n.
proof: Proof. apply (right_cancellation (.*.) (2 ^ n)). rewrite shiftl_negate_nat_pow. transitivity (f x * (2 ^ n // (2 ^ n)↾P2n)); [| ring]. rewrite fields.reciperse_alt. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders