proposition: Lemma lt_succ_le_2 a b: T3nf a -> a < T3succ b -> a <= b.
proof: Proof. elim: a b; first by move => b;rewrite T3le0n. move => a' _ b' _ c' _ n' d' Hd; case; first by rewrite T3lt1 => _ /eqP ->. move => a b c n d nx /=; rewrite all_zeroE; case: eqP => sa. rewrite T3lt_consE => h; rewrite /T3le T3lt_consE sa; move: h. case: (T3ltgtP [a', b', c'] one) => //; first by rewrite orbT. move => h; move: nx;case: h => -> -> ->; rewrite /T3nf => /and5P [ _ _ _ _]. rewrite T3lt1 T3ltn0 if_same if_simpl ltnS leq_eqVlt. move =>/eqP ->; case/orP => h'; rewrite h' ?orbT // (eqP h') ltnn T3eqE. by move: sa; case => -> -> ->; rewrite /= eqxx /= T3lt0n eq_sym; case: eqP. rewrite T3lt_consE => h; rewrite /T3le T3lt_consE; move: h. case: (T3ltgtP [a', b', c'] [a,b,c]) => //;first by rewrite orbT. case => -> -> ->; case: (ltngtP n' n); rewrite ? orbT// => ->. move:nx => /and5P[_ _ _ nd _] /(Hd _ nd) /orP [/eqP -> | ->] //. by rewrite eqxx. by rewrite orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)