proposition: Lemma permut_rev : forall p, permut (rev p) p.
proof: Proof. intros p. apply Permut with (f := fun x => rev_ord x). apply rev_length. apply rev_ord_inj. intros n. simpl. rewrite <- ssrnat.minusE. rewrite rev_length at 2. apply onth_rev. eapply elimT. now apply ssrnat.ltP. now rewrite <- (rev_length p). Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)