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