proposition: Lemma permut_insert : forall v p q, permut (v :: p ++ q) (p ++ v :: q).
proof: Proof. intros v p q. change (permut (((v :: nil) ++ p) ++ q) (p ++ (v :: nil) ++ q)). rewrite app_assoc. apply permut_app_r. apply permut_app. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)