proposition: Lemma rev_behead_etc b l : rev (behead (rev (b :: l))) = belast b l.
proof: Proof. rewrite rev_cons -{2}(revK l). by case: (rev l) => // a s; rewrite /= rev_cons belast_rcons rev_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)