proposition: Lemma QposSumNonNeg : forall l, 0 <= QposSum l.
proof: Proof. induction l. apply: leEq_reflexive. simpl. apply: plus_resp_nonneg. apply: less_leEq. apply Qpos_prf. assumption. Qed.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q