2 files changed, 3 insertions, 40 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 76752c6450..7d8e4b02cb 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -25,32 +25,13 @@ Require Export SplitRmult.
 Require Export ArithProp.
 Require Omega.
 Require Zpower.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+V7only [Import R_scope.].
+Open Local Scope R_scope.
 
 (*******************************)
-(**     Factorial              *)
+(**  Lemmas about factorial    *)
 (*******************************)
 (*********)
-Fixpoint fact [n:nat]:nat:=
-  Cases n of
-     O     => (S O)
-    |(S n) => (mult (S n) (fact n))
-  end.
-
-(*********)
-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 n m;Simpl;Auto.
-Qed.
-
-(*********)
 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.
 Qed.    
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index ca232ccb9a..5961ab8328 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1096,21 +1096,3 @@ Left; Apply pow_lt; Apply Rabsolu_pos_lt; Assumption.
 Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4).
 Apply H1; Assumption.
 Qed.
-
-Lemma fact_growing : (m,n:nat) (le m n) -> (le (fact m) (fact n)).
-Intros.
-Cut (Un_growing [n:nat](INR (fact n))).
-Intro.
-Apply INR_le.
-Apply Rle_sym2.
-Apply (growing_prop [l:nat](INR (fact l))).
-Exact H0.
-Unfold ge; Exact H.
-Unfold Un_growing.
-Intros.
-Simpl.
-Rewrite plus_INR.
-Pattern 1 (INR (fact n0)); Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
-Apply pos_INR.
-Qed.