proposition: Fact le_trans : transitive le.
proof: Proof. move=> y x z; rewrite !le_def; case: eqVneq => [->|_] //=. by case: eqVneq => [-> ->|_ hxy /(lt_trans hxy) ->]; rewrite orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)