proposition: Lemma even_etail et : even_tail (etail et).
proof: Proof. rewrite /etail /etrace_perm; case: ifP; first by rewrite permt_id. by rewrite /even_trace; elim: (ttail et) => [|[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)