proposition: Lemma T1T3_inc x y: (x <y)%ca-> (T1_T3 x) < (T1_T3 y).
proof: Proof. elim: x y; [by case | move => a Ha n b Hb; case => // a' n' b']. rewrite /= T3lt_consE T3lt_psi /lt_psi T3ltnn /=. case: (CantorOrdinal.T1ltgtP a a') => aa' //; first by rewrite Ha //. rewrite aa' T3ltnn eqxx /=. case: (CantorOrdinal.T1ltgtP b b') => bb'; first by rewrite Hb. by rewrite if_same if_simpl => ->. by rewrite if_same if_simpl => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)