proposition: Lemma order_pos_trans : transitive order_pos.
proof: Proof. move=> [x1 y1] [x2 y2] [x3 y3] /= /orP[x2Lx1|/andP[/eqP-> y2Ly1]]. case/orP => [x1Lx3| /andP[/eqP<-]]; last by rewrite x2Lx1. by rewrite (ltn_trans x2Lx1 x1Lx3). by case/orP => [->//|/andP[-> y1Ly3]]; rewrite (leq_trans y2Ly1) // orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)