proposition: Lemma mono_leif (f : T -> T) C : {mono f : x y / x <= y} -> forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).
proof: Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)