proposition: Lemma Boule_half_to_interval : forall x, Boule (/2) posreal_half x -> 0 <= x <= 1.
proof: Proof. unfold Boule, posreal_half; simpl. intros x b; apply Rabs_def2 in b; destruct b; split; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia