proposition: Lemma all_rev l q: all q l = all q (rev l).
proof: Proof. by elim:l => [// | a l hr]; rewrite rev_cons all_rcons /= hr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)