proposition: Lemma T2le_psi_b a b : T2succ b <= [a,b].
proof: Proof. move: (T2lt_psi_b a b). case b => //; first by rewrite T2ge1. move => a1 b1 n1 c1 /= h; apply: T2ltW; move: h. case eq1: ([a1, b1] == one). rewrite !T2lt_consE T2ltn0 ltn0 /= andbF !if_same if_simpl. by move /eqP: eq1 => [ -> ->] ->. by rewrite !T2lt_consE T2ltn0 ltn0 !if_same if_simpl => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)