proposition: Lemma T1T2_inc n p : (n < p)%ca = (T1T2 n < T1T2 p)%g0.
proof: Proof. elim: n p => // [ [] // | a Ha n b Hb [] // a' n' b' /=]. rewrite T2lt_consE /lt_psi eqxx T2ltnn /= Ha Hb - T1T2_inj. by case pa: (T1T2 a < T1T2 a'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)