proposition: Lemma succ_psi_lt x a b c: [a, b, c] != one -> x < [a,b,c] -> T3succ x < [a,b,c].
proof: Proof. move => yn1; case: x => //; first by rewrite /= T3gt1 yn1. move => a' b' c' n d /=; rewrite psi_lt1 all_zeroE; case: eqP. by move => -> h; rewrite T3lt_consE h. by move => sa sb; rewrite T3lt_consE sb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)