proposition: Lemma exp_0 : exp 0 = 1.
proof: Proof. cut (exp_in 0 1). - cut (exp_in 0 (exp 0)). + apply uniqueness_sum. + exact (proj2_sig (exist_exp 0)). - unfold exp_in; unfold infinite_sum; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. + unfold Rdist; replace (1 - 1) with 0; [ rewrite Rabs_R0; assumption | ring ]. + induction n as [| n Hrecn]. * simpl; rewrite Rinv_1; ring. * rewrite tech5. rewrite <- Hrecn. -- simpl. ring. -- unfold ge; apply Nat.le_0_l. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia