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