proposition: Lemma split_le x : (T3split x).1 <= x.
proof: Proof. elim: x => // a _ b _ c _ n d Hd /=. case pa: (all_zero a b c) => //; move: Hd; case (T3split d) => y m /=. rewrite /T3le T3lt_consE !eqxx ltnn T3eqE. by case /orP => ->; rewrite ? eqxx // if_same orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)