proposition: Lemma TT1T3_inj: injective T1_T3.
proof: Proof. move => a b h. by case:(CantorOrdinal.T1ltgtP a b) => lab //; move: (T1T3_inc lab); rewrite h T3ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)