diff --git a/theories/prelude.v b/theories/prelude.v
index 28e2123..147a041 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -15,8 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq.
 Require Import Eqdep ClassicalFacts.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -71,7 +71,7 @@ Proof. by []. Qed.
 
 (* rewrite rule for propositional symmetry *)
 Lemma sym A (x y : A) : x = y <-> y = x.
-Proof. by []. Qed.
+Proof. by split. Qed.
 
 (* selecting a list element *)
 (* should really be in seq.v *)