proposition: Lemma T2lt_psi_aux a b a' b': a < a' -> b < [a', b'] -> [a,b] < [a',b'].
proof: Proof. by move => sa sb; rewrite T2ltE /lt_rec sa sb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)