proposition: Lemma all_rev (T: eqType) P (l: seq T) : all P (rev l) = all P l.
proof: Proof. by apply /allP/allP => H x xi; apply:H; [rewrite mem_rev |rewrite - mem_rev]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)