proposition: Lemma le_le_trans x y z t : z <= x -> y <= t -> x <= y -> z <= t.
proof: Proof. by move=> + /(le_trans _)/[apply]; apply: le_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)