proposition: Lemma T2nf_cons_cons a b n a' b' n' c': T2nf(cons a b n (cons a' b' n' c')) = [&& [a', b'] < [a, b], T2nf a, T2nf b & T2nf(cons a' b' n' c') ].
proof: Proof. simpl;case: (T2nf a);rewrite /= ?andbF //. case: (T2nf b);rewrite /= ? andbF //. rewrite T2lt_consE - T2lt_psi. by case: ([a', b'] < [a, b]); rewrite /= ?andbT // T2ltn0 !if_same andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)