proposition: Lemma DtoQ_slow_correct : DtoQ_slow' = StdQtoQ ∘ DtoStdQ.
proof: Proof. intros x y E. unfold compose. rewrite <- E. clear y E. unfold DtoQ_slow. rewrite rings.preserves_mult, (preserves_int_pow 2), rings.preserves_2. now rewrite (integers.to_ring_unique_alt ZtoQ (StdQtoQ ∘ ZtoStdQ)). 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