diff options
| author | notin | 2006-10-27 13:05:29 +0000 |
|---|---|---|
| committer | notin | 2006-10-27 13:05:29 +0000 |
| commit | 7465eba1019dc082f94b85aab5b7c28ae61c77ef (patch) | |
| tree | 10733c34b8d475ed8e9839bf3383c4ef3d9cf5f7 | |
| parent | 7273f8f1e72fd2d72c6ea54c13895580e66b872d (diff) | |
Le caractère ² fait planter make doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/Rprod.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 758f7b357c..dbf236967e 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -98,7 +98,7 @@ Proof. ring. Qed. -(** We prove that (N!)²<=(2N-k)!*k! forall k in [|O;2N|] *) +(** We prove that (N!)^2<=(2N-k)!*k! forall k in [|O;2N|] *) Lemma RfactN_fact2N_factk : forall N k:nat, (k <= 2 * N)%nat -> |