proposition: Lemma rationals_decompose_le (x y: Q) : x ≤ y → ∃ num, ∃ den, den ≠ 0 ∧ y = x + n_to_sr num * / n_to_sr den.
proof: Proof. Proof with eauto. intros [n [d E]]. destruct (decide (d = 0)) as [A|A]... exists (0%mc:nat), (1%mc:nat). split. discriminate. rewrite E, A, preserves_0, preserves_1, dec_recip_0. ring. Qed.
imports: Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.integers MathClasses.implementations.natpair_integers MathClasses.theory.rationals MathClasses.theory.dec_fields MathClasses.theory.rings MathClasses.orders.integers MathClasses.orders.dec_fields