proposition: Lemma OT_order_le_transitive x y z: x <=t y -> y <=t z -> x <=t z.
proof: Proof. move /OTorder_le_alt2P => [pa pb pc] /OTorder_le_alt2P [pd pe pf]. apply /OTorder_le_alt2P. split => //; apply: (order_le_transitive pc pf). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)