From 4c389d1c425b5b0cc168b6071f2bbcdff80b7597 Mon Sep 17 00:00:00 2001 From: mayero Date: Fri, 10 Nov 2000 22:32:02 +0000 Subject: mise-a-jour, ajouts de quelques truc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@843 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rbase.v | 169 ++++++++++++++++++++++++++++++++++++++++++++ theories/Reals/Rbasic_fun.v | 114 +++++++++++++++++------------- theories/Reals/Rfunctions.v | 41 ++++++++++- 3 files changed, 274 insertions(+), 50 deletions(-) (limited to 'theories') diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index bfbab59bd..b459a3d85 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -224,6 +224,13 @@ Intro;Generalize (H0 r1==R0 r2==R0 (Rmult r1 r2)==R0 Tauto. Save. +(**********) +Lemma Rmult_Rplus_distrl: + (r1,r2,r3:R) ((Rmult (Rplus r1 r2) r3)== + (Rplus (Rmult r1 r3) (Rmult r2 r3))). +Intros; Ring. +Save. + (***********) Definition Rsqr:R->R:=[r:R](Rmult r r). @@ -281,6 +288,13 @@ Intro cla;Apply (cla (Rminus r1 r2)==R0 r1==r2 (Rminus_eq r1 r2));Assumption. Tauto. Save. +(**********) +Lemma Rminus_distr: + (x,y,z:R) (Rmult x (Rminus y z))== + (Rminus (Rmult x y) (Rmult x z)). +Intros; Ring. +Save. + (**********) Lemma eq_Ropp:(r1,r2:R)(r1==r2)->((Ropp r1)==(Ropp r2)). Auto with real. @@ -315,6 +329,28 @@ Intros;Red;Intro;Generalize (Rplus_plus_r r (Ropp r) R0 H0);Intro; Generalize (sym_eqT R R0 r H1);Intro;Auto. Save. +(*********) +Lemma Rinv_R1:(Rinv R1)==R1. +Apply (r_Rmult_mult R1 (Rinv R1) R1); + [Rewrite (Rinv_r R1 R1_neq_R0); + Rewrite (let (H1,H2)=(Rmult_ne R1) in H1);Trivial| + Red;Intro;Apply R1_neq_R0;Assumption]. +Save. + +(*********) +Lemma Rinv_neq_R0:(r:R)(~r==R0)->~(Rinv r)==R0. +Intros;Red;Intro;Generalize (Rmult_mult_r r (Rinv r) R0 H0); + Clear H0;Intro;Rewrite (Rinv_r r H) in H0;Rewrite (Rmult_Or r) in H0; + Generalize R1_neq_R0;Intro;Auto. +Save. + +(*********) +Lemma Rinv_Rinv:(r:R)(~r==R0)->(Rinv (Rinv r))==r. +Intros;Apply (r_Rmult_mult (Rinv r) (Rinv (Rinv r)) r); + [Rewrite (Rinv_r (Rinv r) (Rinv_neq_R0 r H)); + Rewrite (Rinv_l r H);Trivial |Apply Rinv_neq_R0;Assumption]. +Save. + (*********) Lemma Rinv_Rmult:(r1,r2:R)(~r1==R0)->(~r2==R0)-> (Rinv (Rmult r1 r2))==(Rmult (Rinv r1) (Rinv r2)). @@ -374,6 +410,13 @@ Generalize (Rlt_antisym r1 r2 H1); Intro; Auto with zarith real. Elim (imp_not_Req r2 r1);Auto with zarith real. Save. +(**********) +Lemma Rlt_ge_not:(r1,r2:R)(Rlt r1 r2)->~(Rge r1 r2). +Intros;Red;Intro;Unfold Rge in H0;Unfold Rgt in H0;Elim H0;Intro. +Apply (Rlt_antisym r1 r2 H H1). +Rewrite H1 in H;Exact (Rlt_antisym r2 r2 H H). +Save. + (**********) Lemma Rle_le_eq:(r1,r2:R)(Rle r1 r2)/\(Rle r2 r1)<->(r1==r2). Intros; Split; Intro. @@ -492,6 +535,18 @@ Apply (Rlt_anti_compatibility r R0 (Ropp r)); Rewrite (Rplus_Ropp_r r);Assumption. Save. +(**********) +Lemma Rle_monotony: + (r,r1,r2:R) + (Rle R0 r) + ->(Rle r1 r2)->(Rle (Rmult r r1) (Rmult r r2)). +Intros r r1 r2;Unfold Rle;Intros;Elim H;Elim H0;Intros. +Left;Apply Rlt_monotony;Assumption. +Right;Rewrite H1;Reflexivity. +Right;Rewrite <- H2;Rewrite Rmult_Ol;Rewrite Rmult_Ol;Reflexivity. +Right;Rewrite H1;Reflexivity. +Save. + (**********) Lemma Rlt_minus:(r1,r2:R)(Rlt r1 r2)->(Rlt (Rminus r1 r2) R0). Intros; Cut (Rlt (Rminus r1 r2) (Rminus r2 r2)). @@ -646,6 +701,37 @@ Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto. Apply (imp_not_Req r R0);Left;Assumption. Save. +(*********) +Lemma Rinv_lt:(r1,r2:R)(Rlt R0 (Rmult r1 r2))->(Rlt r1 r2)-> + (Rlt (Rinv r2) (Rinv r1)). +Intros;Generalize (Rlt_monotony (Rinv (Rmult r1 r2)) r1 r2 + (Rlt_Rinv (Rmult r1 r2) H) H0);Intro; + Elim (without_div_O_contr r1 r2 + (sym_not_eqT R R0 (Rmult r1 r2) (imp_not_Req R0 (Rmult r1 r2) + (or_introl (Rlt R0 (Rmult r1 r2)) (Rgt R0 (Rmult r1 r2)) H)))); + Intros;Rewrite Rinv_Rmult in H1;Auto; + Rewrite (Rmult_assoc (Rinv r1) (Rinv r2) r2) in H1; + Rewrite (Rinv_l r2 H3) in H1; + Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H1) in H1; + Rewrite (Rmult_sym (Rinv r1) (Rinv r2)) in H1; + Rewrite (Rmult_assoc (Rinv r2) (Rinv r1) r1 ) in H1; + Rewrite (Rinv_l r1 H2) in H1; + Rewrite (let (H1,H2)=(Rmult_ne (Rinv r2)) in H1) in H1;Assumption. +Save. + +(**********) +Lemma Rlt_monotony_rev: + (r,r1,r2:R)(Rlt R0 r)->(Rlt (Rmult r r1) (Rmult r r2)) + ->(Rlt r1 r2). +Intros;Cut (s:R) (Rmult (Rinv r) (Rmult r s))==s. +Intros; Rewrite <- (H1 r1); Rewrite <- (H1 r2);Apply Rlt_monotony. +Apply Rlt_Rinv; Assumption. +Assumption. +Intro;Rewrite <- Rmult_assoc;Rewrite Rinv_l. +Ring. +Apply imp_not_Req; Right; Unfold Rgt; Assumption. +Save. + (*********************************************************) (* Greater *) (*********************************************************) @@ -814,6 +900,14 @@ Left; Apply (Rgt_r_plus_plus r r1 r2 H0). Right; Apply (r_Rplus_plus r r1 r2 H0). Save. +(***********) +Lemma Rge_monotony: + (x,y,z:R) (Rge z R0) -> (Rge x y) -> (Rge (Rmult x z) (Rmult y z)). +Intros;Apply Rle_sym1; + Rewrite (Rmult_sym y z); Rewrite (Rmult_sym x z); + Apply Rle_monotony;Apply Rle_sym2; Assumption. +Save. + (***********) Lemma Rgt_minus:(r1,r2:R)(Rgt r1 r2)->(Rgt (Rminus r1 r2) R0). Intros; Cut (Rgt (Rminus r1 r2) (Rminus r2 r2)). @@ -823,6 +917,16 @@ Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2)); Apply (Rgt_plus_plus_r (Ropp r2) r1 r2 H). Save. +(*********) +Lemma minus_Rgt:(r1,r2:R)(Rgt (Rminus r1 r2) R0)->(Rgt r1 r2). +Intros;Generalize (Rgt_plus_plus_r r2 (Rminus r1 r2) R0 H); Intro; + Rewrite (Rplus_sym r2 (Rminus r1 r2)) in H0;Unfold Rminus in H0; + Rewrite (Rplus_assoc r1 (Ropp r2) r2) in H0; + Rewrite (Rplus_Ropp_l r2) in H0; + Elim (Rplus_ne r1); Intros a b; Rewrite a in H0; Clear a b; + Elim (Rplus_ne r2); Intros a b; Rewrite a in H0; Clear a b;Exact H0. +Save. + (**********) Lemma Rge_minus:(r1,r2:R)(Rge r1 r2)->(Rge (Rminus r1 r2) R0). Unfold Rge; Intros; Elim H; Intro. @@ -846,6 +950,12 @@ Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro; Rewrite (Rmult_Or r1) in H1;Assumption. Save. +(*********) +Lemma Rmult_lt_pos:(x,y:R)(Rlt R0 x)->(Rlt R0 y)->(Rlt R0 (Rmult x y)). +Generalize Rmult_gt;Unfold Rgt;Auto. +Save. + + (***********) Lemma Rplus_eq_R0:(a,b:R)(Rle R0 a)->(Rle R0 b)->(Rplus a b)==R0-> (a==R0)/\(b==R0). @@ -919,6 +1029,34 @@ Unfold Rminus; Rewrite -> Rplus_sym; Rewrite -> Rplus_assoc; Auto with zarith real. Save. +(*********) +Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)). +Induction n. +Simpl; Intro;Apply sym_eqT;Apply Rmult_Ol. +Intros;Unfold 1 mult;Cbv Beta Iota;Fold mult; + Rewrite (plus_INR m (mult n0 m));Rewrite (H m); + Pattern 1 (INR m); + Rewrite <-(let (H1,H2)=(Rmult_ne (INR m)) in H1); + Rewrite (Rmult_sym (INR n0) (INR m)); + Rewrite <-(Rmult_Rplus_distr (INR m) R1 (INR n0)); + Rewrite (Rplus_sym R1 (INR n0));Rewrite <-(S_INR n0); + Apply Rmult_sym. +Save. + + +(*********) +Lemma INR_lt_0:(n:nat)(lt O n)->(Rlt R0 (INR n)). +Induction n;Intros. +Absurd (lt (0) (0));[Apply lt_n_n|Assumption]. +Elim (le_lt_or_eq (0) n0 (lt_n_Sm_le (0) n0 H0));Intro. +Generalize (H H1);Clear H H1;Intro;Rewrite (S_INR n0); + Generalize (Rlt_compatibility R1 R0 (INR n0) H);Intro; + Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1; + Rewrite (Rplus_sym (INR n0) R1); + Apply (Rlt_trans R0 R1 (Rplus R1 (INR n0)) (Rlt_R0_R1) H1). +Rewrite <-H1;Simpl;Apply Rlt_R0_R1. +Save. + (**********) Lemma INR_le:(n:nat)(Rle R0 (INR n)). Induction n. @@ -927,6 +1065,18 @@ Intros;Rewrite (S_INR n0);Apply (Rlt_le R0 (Rplus (INR n0) R1)); Apply (Rlt_r_plus_R1 (INR n0) H). Save. +(*********) +Lemma INR_le_nm:(n,m:nat)(le n m)->(Rle (INR n) (INR m)). +Intros;Elim (le_lt_or_eq n m H);Intro. +Cut (lt (0) (minus m n)). +Intro;Generalize (INR_lt_0 (minus m n) H1); + Intro;Rewrite minus_INR in H2;Auto; + Apply (Rlt_le (INR n) (INR m));Fold (Rgt (INR m) (INR n)); + Apply (minus_Rgt (INR m) (INR n));Unfold Rgt;Assumption. +Omega. +Rewrite H0;Unfold Rle;Right;Trivial. +Save. + (**********) Lemma not_INR_O:(n:nat)~(INR n)==R0->~n=O. Intros;Cut n=(0)->(INR n)==R0. @@ -951,6 +1101,11 @@ Save. (**********) Definition INZ:=inject_nat. +(**********) +Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)). +Unfold INZ;Intros;Apply inject_nat_complete;Assumption. +Save. + (**********) Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)). Induction n;Auto with zarith real. @@ -1077,6 +1232,14 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); Intro;Omega. Save. +(*********) +Lemma le_O_IZR:(z:Z)(Rle R0 (IZR z))->(Zle ZERO z). +Unfold Rle;Intros;Elim H;Clear H;Intro. +Unfold Zle;Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H)); + Assumption. +Generalize (eq_IZR_R0 z (sym_eqT R R0 (IZR z) H));Intro;Omega. +Save. + (**********) Lemma le_IZR_R1:(z:Z)(Rle (IZR z) R1)->(Zle z `1`). Induction z; Intros. @@ -1105,6 +1268,12 @@ Right;Cut (R1==(IZR `1`));Auto with zarith real. Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (NEG p) `1` H0). Save. +(**********) +Lemma IZR_ge: + (m,n:Z) `m>= n` ->(Rge (IZR m) (IZR n)). +Intros;Apply Rlt_not_ge;Red;Intro;Generalize (lt_IZR m n H0);Intro; Omega. +Save. + (**********) Lemma single_z_r_R1:(r:R)(z,x:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1)) ->(Rlt r (IZR x))->(Rle (IZR x) (Rplus r R1))->z=x. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 63b9a3cfb..b7466eb87 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -19,18 +19,31 @@ Definition Rmin :R->R->R:=[x,y:R] | (rightT _) => y end. +(*********) +Lemma Rmin_Rgt_l:(r1,r2,r:R)(Rgt (Rmin r1 r2) r) -> + ((Rgt r1 r)/\(Rgt r2 r)). +Intros r1 r2 r;Unfold Rmin;Case (total_order_Rle r1 r2);Intros. +Split. +Assumption. +Unfold Rgt;Unfold Rgt in H;Exact (Rlt_le_trans r r1 r2 H r0). +Split. +Generalize (not_Rle r1 r2 n);Intro;Exact (Rgt_trans r1 r2 r H0 H). +Assumption. +Save. + +(*********) +Lemma Rmin_Rgt_r:(r1,r2,r:R)(((Rgt r1 r)/\(Rgt r2 r)) -> + (Rgt (Rmin r1 r2) r)). +Intros;Unfold Rmin;Case (total_order_Rle r1 r2);Elim H;Clear H;Intros; + Assumption. +Save. + (*********) Lemma Rmin_Rgt:(r1,r2,r:R)(Rgt (Rmin r1 r2) r)<-> ((Rgt r1 r)/\(Rgt r2 r)). -Intros;Split. -Unfold Rmin;Case (total_order_Rle r1 r2);Intros. -Split;Auto. -Unfold Rgt in H;Unfold Rgt;Apply (Rlt_le_trans r r1 r2 H r0). -Split;Auto. -Generalize (not_Rle r1 r2 n);Intro;Clear n; - Apply (Rgt_trans r1 r2 r H0 H). -Intro;Elim H;Intros;Clear H;Unfold Rmin;Case (total_order_Rle r1 r2); - Intros;Auto. +Intros; Split. +Exact (Rmin_Rgt_l r1 r2 r). +Exact (Rmin_Rgt_r r1 r2 r). Save. (*******************************) @@ -85,6 +98,22 @@ Intros;Unfold Rabsolu;Case (case_Rabsolu r);Intro;Auto. Apply Ropp_neq;Auto. Save. +(*********) +Lemma Rabsolu_left: (r:R)(Rlt r R0)->((Rabsolu r) == (Ropp r)). +Intros;Unfold Rabsolu;Case (case_Rabsolu r);Trivial;Intro;Absurd (Rge r R0). +Exact (Rlt_ge_not r R0 H). +Assumption. +Save. + +(*********) +Lemma Rabsolu_right: (r:R)(Rge r R0)->((Rabsolu r) == r). +Intros;Unfold Rabsolu;Case (case_Rabsolu r);Intro. +Absurd (Rge r R0). +Exact (Rlt_ge_not r R0 r0). +Assumption. +Trivial. +Save. + (*********) Lemma Rabsolu_pos:(x:R)(Rle R0 (Rabsolu x)). Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro. @@ -93,6 +122,17 @@ Generalize (Rlt_Ropp x R0 r);Intro;Unfold Rgt in H; Apply Rle_sym2;Assumption. Save. +(*********) +Lemma Rabsolu_pos_eq:(x:R)(Rle R0 x)->(Rabsolu x)==x. +Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro; + [Generalize (Rle_not R0 x r);Intro;ElimType False;Auto|Trivial]. +Save. + +(*********) +Lemma Rabsolu_Rabsolu:(x:R)(Rabsolu (Rabsolu x))==(Rabsolu x). +Intro;Apply (Rabsolu_pos_eq (Rabsolu x) (Rabsolu_pos x)). +Save. + (*********) Lemma Rabsolu_pos_lt:(x:R)(~x==R0)->(Rlt R0 (Rabsolu x)). Intros;Generalize (Rabsolu_pos x);Intro;Unfold Rle in H0; @@ -249,46 +289,22 @@ Save. (*********) Lemma Rabsolu_triang_inv:(a,b:R)(Rle (Rminus (Rabsolu a) (Rabsolu b)) (Rabsolu (Rminus a b))). -Intros;Unfold Rabsolu;Case (case_Rabsolu a);Case (case_Rabsolu b); - Case (case_Rabsolu (Rminus a b));Intros. -Unfold Rle;Right;Rewrite (Ropp_distr2 a b);Unfold Rminus; - Rewrite Ropp_Ropp;Apply Rplus_sym. -Unfold 1 Rminus;Rewrite Ropp_Ropp;Rewrite Rplus_sym; - Fold (Rminus b a);Generalize (minus_Rge a b r);Intro; - Generalize (Rle_sym2 b a H);Intro;Generalize (Rle_minus b a H0); - Intro;Generalize (Rle_sym2 R0 (Rminus a b) r);Intro; - Apply (Rle_trans (Rminus b a) R0 (Rminus a b) H1 H2). -Rewrite (Ropp_distr2 a b);Unfold Rminus; - Rewrite (Rplus_sym b (Ropp a));Apply Rle_compatibility; - Unfold Rge in r0;Elim r0;Intros. -Unfold Rle;Left;Generalize (Rgt_RoppO b H);Intro;Unfold Rgt in H; - Apply (Rlt_trans (Ropp b) R0 b H0 H). -Unfold Rle;Right;Rewrite H;Apply Ropp_O. -Generalize (minus_Rge a b r);Intro; - Generalize (Rge_trans a b R0 H r0);Intro; - Generalize (Rlt_antisym a R0 r1);Intro; - Unfold Rge in H0;Elim H0;Intro. -Unfold Rgt in H2;ElimType False;Auto. -Rewrite H2 in r1;Generalize (Rlt_antirefl R0);Intro;ElimType False; - Auto. -Generalize (Rminus_lt a b r);Intro;Generalize (Rlt_trans a b R0 H r0); - Intro;Unfold Rge in r1;Elim r1;Intro. -Generalize (Rlt_antisym a R0 H0);Intro;Unfold Rgt in H1;ElimType False; - Auto. -Rewrite H1 in H0;Generalize (Rlt_antirefl R0);Intro;ElimType False; - Auto. -Unfold Rminus;Apply Rle_compatibility;Rewrite Ropp_Ropp; - Generalize (Rlt_compatibility (Ropp b) b R0 r0);Intro; - Rewrite Rplus_Ropp_l in H; - Rewrite (let (H1,H2)=(Rplus_ne (Ropp b)) in H1) in H; - Generalize (Rlt_trans b R0 (Ropp b) r0 H);Intro; - Apply Rlt_le;Assumption. -Generalize (Rlt_compatibility (Ropp (Rminus a b)) (Rminus a b) R0 r); -Intro; Rewrite Rplus_Ropp_l in H; - Rewrite (let (H1,H2)=(Rplus_ne (Ropp (Rminus a b))) in H1) in H; - Generalize (Rlt_trans (Rminus a b) R0 (Ropp (Rminus a b)) r H);Intro; - Apply Rlt_le;Assumption. -Unfold Rle;Right;Trivial. +Intros; + Apply (Rle_anti_compatibility (Rabsolu b) + (Rminus (Rabsolu a) (Rabsolu b)) (Rabsolu (Rminus a b))); + Unfold Rminus; + Rewrite <- (Rplus_assoc (Rabsolu b) (Rabsolu a) (Ropp (Rabsolu b))); + Rewrite (Rplus_sym (Rabsolu b) (Rabsolu a)); + Rewrite (Rplus_assoc (Rabsolu a) (Rabsolu b) (Ropp (Rabsolu b))); + Rewrite (Rplus_Ropp_r (Rabsolu b)); + Rewrite (proj1 ? ? (Rplus_ne (Rabsolu a))); + Replace (Rabsolu a) with (Rabsolu (Rplus a R0)). + Rewrite <- (Rplus_Ropp_r b); + Rewrite <- (Rplus_assoc a b (Ropp b)); + Rewrite (Rplus_sym a b); + Rewrite (Rplus_assoc b a (Ropp b)). + Exact (Rabsolu_triang b (Rplus a (Ropp b))). + Rewrite (proj1 ? ? (Rplus_ne a));Trivial. Save. (*********) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index c0ade34e1..c030cb4a0 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -17,7 +17,45 @@ Fixpoint fact [n:nat]:nat:= O => (S O) |(S n) => (mult (S n) (fact n)) end. + +(*********) +(*Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O. +Double Induction 1 2;Simpl;Auto. +Save.*) +(*********) +Lemma fact_neq_0:(n:nat)~(fact n)=O. +Cut (n,m:nat)~n=O->~m=O->~(mult n m)=O. +Intro;Induction n;Simpl;Auto. +Intros; Replace (plus (fact n0) (mult n0 (fact n0))) with + (mult (fact n0) (plus n0 (1))). +Cut ~(plus n0 (1))=O. +Intro;Apply H;Assumption. +Replace (plus n0 (1)) with (S n0);[Auto|Ring]. +Intros;Ring. +Double Induction 1 2;Simpl;Auto. +Save. + +(*********) +Lemma INR_fact_neq_0:(n:nat)~(INR (fact n))==R0. +Intro;Red;Intro;Apply (not_O_INR (fact n) (fact_neq_0 n));Assumption. +Save. + +(*********) +Lemma simpl_fact:(n:nat)(Rmult (Rinv (INR (fact (S n)))) + (Rinv (Rinv (INR (fact n)))))== + (Rinv (INR (S n))). +Intro;Rewrite (Rinv_Rinv (INR (fact n)) (INR_fact_neq_0 n)); + Unfold 1 fact;Cbv Beta Iota;Fold fact; + Rewrite (mult_INR (S n) (fact n)); + Rewrite (Rinv_Rmult (INR (S n)) (INR (fact n))). +Rewrite (Rmult_assoc (Rinv (INR (S n))) (Rinv (INR (fact n))) + (INR (fact n)));Rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n)); + Apply (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1). +Apply not_O_INR;Auto. +Apply INR_fact_neq_0. +Save. + (*******************************) (* Power *) (*******************************) @@ -86,6 +124,7 @@ Definition sum_f [s,n:nat;f:nat->R]:R:= (*******************************) (*********) Definition infinit_sum:(nat->R)->R->Prop:=[s:nat->R;l:R] - (eps:R)(Ex[N:nat](n:nat)(ge n N)/\(Rlt (R_dist (sum_f_R0 s n) l) eps)). + (eps:R)(Rgt eps R0)-> + (Ex[N:nat](n:nat)(ge n N)->(Rlt (R_dist (sum_f_R0 s n) l) eps)). -- cgit v1.2.3