proposition: Lemma split_le x : (T1split x).1 <= x.
proof: Proof. elim: x => // a _ n b Hb /=. case pa: (a==zero) => //; move: Hb; case: (T1split b) => y m /=. by rewrite T1le_consE !eqxx /= => ->; rewrite !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)