proposition: Lemma DtoQ_slow_preserves_plus x y : DtoQ_slow' (x + y) = DtoQ_slow' x + DtoQ_slow' y.
proof: Proof. destruct x as [xn xe], y as [yn ye]. unfold plus at 1. unfold DtoQ_slow, dy_plus. simpl. case (decide_rel (≤) xe ye); intros E; simpl. rewrite rings.preserves_plus, ZtoQ_shift. rewrite (lattices.meet_l xe ye) by assumption. ring_simplify. rewrite <-associativity, <-int_pow_exp_plus. now setoid_replace (ye - xe + xe) with ye by ring. now apply (rings.is_ne_0 (2:Q)). rewrite rings.preserves_plus, ZtoQ_shift. rewrite lattices.meet_r. ring_simplify. rewrite <-associativity, <-int_pow_exp_plus. now setoid_replace (xe - ye + ye) with xe by ring. now apply (rings.is_ne_0 (2:Q)). now apply orders.le_flip. 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