proposition: Lemma tail_lt_cons a n b: b < phi0 a -> b < cons a n b.
proof: Proof. case b => // a' n' b' /=. by case: (T1ltgtP a' a) => //; rewrite T1ltn0 if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)