proposition: Lemma succ_is_add_one a: T2succ a = a + one.
proof: Proof. elim:a => // a _ b _ n c Hc /=; rewrite addn0 Hc. case:(T2ltgtP [a, b] one) => //; first by rewrite T2lt1 //. by case => -> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)