proposition: Lemma T1toB_mon2 x y: T1nf x -> T1nf y -> (x < y <-> T1toB x <o T1toB y).
proof: Proof. move => ha hb. case:T1ltgtP => h. by split =>//; move:(T1toB_mon1 hb ha h) => [hc _] /(oleNgt hc). split =>// _; exact:(T1toB_mon1 ha hb h). by rewrite h; split => // [] [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)