proposition: Lemma perm_sym s1 s2 : perm s1 s2 <-> perm s2 s1.
proof: Proof. suff L: forall s1 s2, perm s1 s2 -> perm s2 s1 by split; apply: L. apply: perm_ind=>s1' s2'. - by move=>->->; apply: permutation_nil. - by move=>x t1 t2 -> -> H1; apply: permutation_skip. - by move =>x y t -> ->; apply: permutation_swap eq_refl eq_refl. by move=>t _ H1 _ H2; apply: permutation_trans H2 H1. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)