proposition: Lemma rationals_decompose_pos_den x : ∃ num, ∃ den, 0 < den ∧ x = f num / f den.
proof: Proof. destruct (rationals_decompose x) as [num [den [E1 E2]]]. destruct (total (≤) den 0). exists (-num), (-den). split. apply lt_iff_le_ne. split. now apply rings.flip_nonpos_negate. apply not_symmetry. now apply flip_negate_ne_0. rewrite 2!preserves_negate. rewrite E2. field. split. apply flip_negate_ne_0. now apply injective_ne_0. now apply injective_ne_0. exists num. exists den. split; try assumption. apply lt_iff_le_ne. split. assumption. now apply not_symmetry. 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