proposition: Lemma Qcplus_le_compat : forall x y z t, x<=y -> z<=t -> x+z <= y+t.
proof: Proof. unfold Qcplus, Qcle; intros; simpl in *. repeat rewrite Qred_correct. apply Qplus_le_compat; auto. Qed.
imports: Field QArith Znumtheory Eqdep_dec