proposition: Lemma leq_lt_trans r x y z: order r -> gle r x y -> glt r y z -> glt r x z.
proof: Proof. move=> or le1 [le2 nxy]; split; first by apply: order_transitivity le1 le2. dneg xz; rewrite xz in le1. apply: (order_antisymmetry or le2 le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)