proposition: Lemma conv_fnorm f g : increasing f -> increasing g -> conv (fnorm f) (fnorm g) =1 fnorm (conv f g).
proof: Proof. move=> fI gI i. rewrite /fnorm /conv /= -bigmin_constB subnn. apply: bigmin_ext => j. by rewrite addnBA ?increasingE // addnBAC ?increasingE // subnDA. Qed.
imports: mathcomp(all_ssreflect finmap)