proposition: Lemma all_permut : forall P p q, all P p -> permut p q -> all P q.
proof: Proof. intros P p q. revert p. induction q as [|v q IH] ; intros p Hp Hpq. easy. assert (Hpv := Hpq). apply permut_sym, permut_remove in Hpv. destruct Hpv as [s [t [Hpv Hq]]]. apply permut_sym in Hq. cut (P v /\ all P (s ++ t)). intros [H1 H2]. apply (conj H1). now apply IH with (2 := Hq). rewrite Hpv in Hp. clear -Hp. induction s as [|h p IH]. exact Hp. destruct Hp as [H1 H2]. destruct (IH H2) as [H3 H4]. apply (conj H3). easy. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)