proposition: Fact trans: transitive le.
proof: Proof. elim=> [|y sy ihs] [|x sx] [|z sz] //=; case: (comparableP x y) => //= [xy|->]. by move=> _ /andP[/(lt_le_trans xy) xz _]; rewrite (ltW xz)// lt_geF. by case: comparableP => //= _; apply: ihs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)