proposition: Lemma split_le x : (T2split x).1 <= x.
proof: Proof. elim: x => // a _ b _ n c Hc /=. case pa:([a, b] == one) => //; move: Hc; case (T2split c) => y m /=. by rewrite T2le_consE !eqxx ltnn => -> /=; rewrite if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)