proposition: Lemma lt_succ_succE x y: T3nf x -> T3nf y -> (T3succ x < T3succ y) = (x < y).
proof: Proof. move => nx ny. case (T3ltgtP (T3succ x) (T3succ y)). + by move/lt_succ_succ => ->. + by move /lt_succ_succ => /T3lt_anti. + by move /eqP; rewrite (succ_inj nx ny) => /eqP ->; rewrite T3ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)