proposition: Lemma cond_positivity_car: forall x, cond_positivity x = true <-> 0 <= x.
proof: Proof. intro ; unfold cond_positivity ; destruct (Rle_dec 0 x) ; intuition ; discriminate. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity