proposition: Lemma permut_trans : forall q p r, permut p q -> permut q r -> permut p r.
proof: Proof. intros q p r [Hl1 f1 Hf1 Hpq] [Hl2 f2 Hf2 Hqr]. revert f1 Hf1 Hpq f2 Hf2 Hqr. rewrite <- Hl1. intros f1 Hf1 Hpq f2 Hf2 Hqr. apply Permut with (f := fun k => f2 (f1 k)). now apply eq_trans with (length q). now apply inj_comp. intros n. now rewrite <- Hqr. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)