diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Int31/Cyclic31.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 1be361b66..98f84a60c 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -654,7 +654,7 @@ Section Basics. f_equal; auto. Qed. - (** This equivalence allows to prove easily the following delicate + (** This equivalence allows proving easily the following delicate result *) Lemma EqShiftL_twice_plus_one : forall k x y, |