proposition: Lemma head_lt_cons a n b: a < cons a n b.
proof: Proof. by elim : a n b => // a Ha n b _ n' b' /=; rewrite (Ha n b). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)