proposition: Lemma shiftl_negate_nat_pow x n : f (x ≪ (-g n)) * 2 ^ n = f x.
proof: Proof. pose proof nat_pow_proper. pattern n. apply naturals.induction; clear n. solve_proper. rewrite rings.preserves_0, rings.negate_0, shiftl_0. rewrite nat_pow_0. ring. intros n E. rewrite rings.preserves_plus, rings.preserves_1. etransitivity; [| eassumption]. setoid_replace (-g n) with (1 - (1 + g n)) by ring. rewrite shiftl_S, rings.preserves_mult, rings.preserves_2. rewrite nat_pow_S. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders