Deplacement lemmes sur fact de Reals vers Arith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 19 insertions, 40 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index 720a8d977c..04dfd287fc 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -43,6 +43,7 @@ let translate_v7_string = function
   | "max_sym" -> "max_comm"
   | "min_sym" -> "min_comm"
   | "gt_not_sym" -> "gt_asym"
+  | "fact_growing" -> "fact_le"
   (* Bool *)
   | "orb_sym" -> "orb_comm"
   | "andb_sym" -> "andb_comm"
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 4963379e68..71cef55ce4 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -9,7 +9,10 @@
 (*i $Id$ i*)
 
 Require Plus.
+Require Mult.
 Require Lt.
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
 
 (** Factorial *)
 
@@ -32,3 +35,15 @@ Apply lt_O_neq.
 Apply lt_O_fact.
 Qed.
 
+Lemma fact_growing : (m,n:nat) (le m n) -> (le (fact m) (fact n)).
+Proof.
+NewInduction 1.
+Apply le_n.
+Assert (le (mult (S O) (fact m)) (mult (S m0) (fact m0))).
+Apply le_mult_mult.
+Apply lt_le_S; Apply lt_O_Sn.
+Assumption.
+Simpl (mult (S O) (fact m)) in H0.
+Rewrite <- plus_n_O in H0.
+Assumption.
+Qed.
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.