proposition: Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p.
proof: Proof. unfold Qclt, Qcplus, Qcopp; intros; simpl in *. repeat rewrite Qred_correct. apply Qlt_minus_iff; auto. Qed.
imports: Field QArith Znumtheory Eqdep_dec