proposition: Lemma pred_le a: T3pred a <= a.
proof: Proof. elim: a => // a _ b _ c _ n d Hd /=;rewrite all_zeroE; case: eqP. case => -> -> ->; case: n => // n; apply:T3ltW; rewrite T3lt_consE. by rewrite T3ltnn eqxx ltnS leqnn. move => _; rewrite /T3le T3lt_consE T3ltnn ! eqxx ltnn T3eqE. by case /orP: Hd => ->; rewrite ?orbT // !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)