proposition: Lemma mono_leqif f : {mono f : m n / m <= n} -> forall m n C, (f m <= f n ?= iff C) = (m <= n ?= iff C).
proof: Proof. by move=> f_mono m n C; rewrite /leqif !eqn_leq !f_mono. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring