proposition: Lemma T1toB_injective x y: T1nf x -> T1nf y -> T1toB x = T1toB y -> x = y.
proof: Proof. move => ha hb. case /or3P: (T1lt_trichotomy x y). + by move/(T1toB_mon1 ha hb) => []. + by move /eqP. + by move/(T1toB_mon1 hb ha) => [_ /nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)