proposition: Lemma onth_rev : forall n p, n < length p -> onth n (rev p) = onth (length p - S n) p.
proof: Proof. intros n [|h p]. easy. intros H. rewrite 2!onth_nth with (d := h). now rewrite rev_nth with (1 := H). lia. now rewrite rev_length. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)