diff options
| -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 -> |