diff options
| -rw-r--r-- | theories/Arith/Factorial.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 0871c4af67..f87d7e810a 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -33,7 +33,7 @@ Qed. Lemma fact_le n m : n <= m -> fact n <= fact m. Proof. - induction 1. + induction 1 as [|m ?]. - apply le_n. - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. |