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