proposition: Lemma div2_S_double : forall N:nat, Nat.div2 (S (2 * N)) = N.
proof: Proof. intro; induction N as [| N HrecN]. - reflexivity. - replace (2 * S N)%nat with (S (S (2 * N))). + simpl; simpl in HrecN; rewrite HrecN; reflexivity. + ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra