proposition: Lemma DtoQ_correct : DtoQ' = DtoQ_slow'.
proof: Proof. intros x y E. rewrite <-E. clear y E. unfold DtoQ, DtoQ_slow. destruct x as [xm xe]. simpl. case (decide_rel); intros E. now rewrite ZtoQ_shift. rewrite int_pow_negate_alt, ZtoQ_shift. now rewrite rings.preserves_1, left_identity. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals MathClasses.implementations.nonneg_integers_naturals MathClasses.implementations.stdlib_rationals MathClasses.theory.rationals MathClasses.theory.shiftl MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.theory.abs