diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-14 00:11:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-14 00:11:56 +0000 |
| commit | 971a4e00a56cb142fb5fb2ef1fe3b87a14f488b6 (patch) | |
| tree | 4fb10f9dfa12a80a2b4f1ec2359d80c01e18425b /theories/Reals/SeqProp.v | |
| parent | d667cf4a1463e82569b497f38bef6eac1955f409 (diff) | |
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
Diffstat (limited to 'theories/Reals/SeqProp.v')
| -rw-r--r-- | theories/Reals/SeqProp.v | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index ca232ccb9..5961ab832 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. |