proposition: Lemma succ_lt a: a < T1succ a.
proof: Proof. elim: a => // a asa n b bb;move: asa; case: a; first by rewrite /= ltnSn. by move => u v w h /=; rewrite bb ! eqxx !ltnn if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)