proposition: Lemma imo_osr: order_on (increasing_mappings_order r r') (increasing_mappings r r').
proof: Proof. move: (order_function_osr (substrate r) or'(erefl (substrate r'))) => [pa pb]. apply:(iorder_osr pa); rewrite pb; apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)