proposition: Lemma T2toB_injective x y: T2nf x -> T2nf y -> T2toB x = T2toB y -> x = y.
proof: Proof. move => ha hb. case /or3P: (T2lt_trichotomy x y). + by move/(T2toB_mon1 ha hb) => []. + by move /eqP. + by move/(T2toB_mon1 hb ha) => [_ /nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)