proposition: Lemma permut_remove : forall v p q, permut (v :: p) q -> exists s, exists t, q = s ++ v :: t /\ permut p (s ++ t).
proof: Proof. intros v p q H. destruct (H) as [Hl f Hf H']. specialize (H' (@ord0 (length p))). revert H'. generalize (nat_of_ord (f (@ord0 (length p)))). simpl. intros n. intros H'. clear -H H'. apply eq_sym in H'. destruct onth_insert with (1 := H') as [r [s Hq]]. exists r, s. apply (conj Hq). rewrite Hq in H. clear -H. apply permut_cons_rev with v. apply permut_trans with (1 := H). apply permut_sym, permut_insert. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)