proposition: Lemma pred_lt a: T3is_succ a -> T3pred a < a.
proof: Proof. elim: a => // a _ b _ c _ n d Hd /=; rewrite all_zeroE; case: eqP. by move => h; case: n => // n _; rewrite T3lt_consE h T3ltnn eqxx ltnS leqnn. by move => /= _ h; rewrite T3lt_consE Hd // !eqxx !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)