proposition: Lemma pred_le a: T1pred a <= a.
proof: Proof. elim: a => // a _ n b Hb /=; case az: (a==zero). by rewrite (eqP az); case: n => // m /=; rewrite T1le_consE /= ltnS leqnn. by rewrite T1le_consE /= Hb !eqxx !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)