proposition: Lemma T2toB_mon2 x y: T2nf x -> T2nf y -> (x < y <-> T2toB x <o T2toB y).
proof: Proof. move => ha hb. case:T2ltgtP => h. by split =>//; move:(T2toB_mon1 hb ha h) => [hc _] => /(oleNgt hc). split =>// _; exact:(T2toB_mon1 ha hb h). by rewrite h; split => // [] [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)