proposition: Lemma phi0_lt1 a n b a': (cons a n b < phi0 a') = (a < a').
proof: Proof. by rewrite /phi0/= T1ltn0 !if_same if_simpl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)