proposition: Lemma increasing_conv f g : increasing f -> increasing g -> increasing (conv f g).
proof: Proof. move=> fI gI i. apply/bigmin_leqP => j. case: ltngtP => // [jLi | ->] _. by apply: bigmin_inf (_ : j <= i) _; rewrite // leq_add2l subSn. rewrite subnn. by apply: bigmin_inf (leqnn i) _; rewrite subnn leq_add2r. Qed.
imports: mathcomp(all_ssreflect finmap)