proposition: Lemma imo_incr f g: gle (increasing_mappings_order r r') f g -> forall i, inc i (substrate r) -> gle r' (Vf f i) (Vf g i).
proof: Proof. by move /imo_gleP => [_ _ [_ _]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)