proposition: Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < Nat.div2 N)%nat.
proof: Proof. intros; induction N as [| N HrecN]. - elim (Nat.nlt_0_r _ H). - cut ((1 < N)%nat \/ N = 1%nat). { intro; elim H0; intro. - destruct N; cbn; [ auto | apply Nat.lt_0_succ ]. - subst N; simpl; apply Nat.lt_0_succ. } inversion H. + right; reflexivity. + left; apply Nat.lt_le_trans with 2%nat; [ apply Nat.lt_succ_diag_r | assumption ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra