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