proposition: Lemma head_rev (T: Type) (a:T) l: head a (rev l) = last a l.
proof: Proof. by elim: l a => // a l H b; rewrite rev_cons - cats1 /= -H;case: rev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)