proposition: Lemma succ_psi_lt2 a b c x: [a, b, c] != one -> ([a, b, c] <= T3succ x) = ([a, b, c] <= x).
proof: Proof. move => ha;symmetry. case (T3leP [a, b, c] (T3succ x)). by rewrite !T3leNgt; apply: contra; apply:succ_psi_lt. by move => hb; move: (T3lt_trans (succ_lt x) hb);rewrite T3ltNge; move /negbTE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)