proposition: Lemma inl_remark_compat: inl_map_compat inl_remark_S inl_remark_ui inl_remark_U.
proof: Proof. rewrite /inl_remark_ui; split; aww. move => i iI; rewrite LgV//; apply:(ci_fp (inl_remark_sub iI)). move => i j /= leij. move:(arg1_sr leij) (arg2_sr leij); rewrite sr => iI jI; rewrite ! LgV//; aw. by apply:(ci_compose (@Fmon _ _ leij) (inl_remark_sub jI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)