proposition: Lemma le_succ_succE x y: T3nf x -> T3nf y -> (T3succ x <= T3succ y) = (x <= y).
proof: Proof. by move => na nb; rewrite /T3le (succ_inj na nb) (lt_succ_succE na nb). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)