proposition: Fact trans : transitive le.
proof: Proof. move=> [y y'] [x x'] [z z'] /andP[/= lexy lexy'] /andP[/= leyz leyz']. rewrite /= /le (le_trans lexy) //=; apply/implyP => lezx. elim: _ / (@le_anti _ _ x y) in y' z' lexy' leyz' *; last first. by rewrite lexy (le_trans leyz). elim: _ / (@le_anti _ _ x z) in z' leyz' *; last by rewrite (le_trans lexy). by rewrite lexx !tagged_asE/= in lexy' leyz' *; rewrite (le_trans lexy'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)