proposition: Lemma Qpos_sum_nonneg : forall l, 0 <= Qpos_sum l.
proof: Proof. induction l. apply Qle_refl. simpl. apply (Qle_trans _ (0+0) _ (Qle_refl _)). apply Qplus_le_compat. destruct a. apply Qlt_le_weak, q. exact IHl. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder