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