proposition: Fact le_trans : transitive le.
proof: Proof. move=> y x z; rewrite !le_def => /eqP lexy /eqP leyz; apply/eqP. by rewrite -[in LHS]lexy -meetA leyz lexy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)