proposition: Lemma permut_sym : forall p q, permut p q -> permut q p.
proof: Proof. intros p q [Hl f Hf Hpq]. revert f Hf Hpq. rewrite Hl. intros f Hf Hpq. apply Permut with (f := invF Hf). now apply eq_sym. apply can_inj with (g := f). apply f_invF. intros n. rewrite <- (f_invF Hf n) at 1. apply eq_sym, Hpq. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)