proposition: Lemma increasing_fmerge f g : increasing f -> increasing g -> increasing (fmerge f g).
proof: Proof. move=> fI gI n; rewrite !fmergeE //. apply/bigmax_leqP => /= i _. apply: leq_trans (leq_bigmax_cond _ (isT : xpredT (inord i : 'I_n.+2))). rewrite inordK ?(leq_trans (ltn_ord _)) //. rewrite leq_min geq_minl /= (leq_trans (geq_minr _ _)) //. apply: increasingE gI _. by rewrite leq_sub2r. Qed.
imports: mathcomp(all_ssreflect finmap)