proposition: Lemma soimP f: inc f (increasing_mappings r r') <-> ((function_prop f (substrate r) (substrate r')) /\ increasing_fun f r r').
proof: Proof. split; first by move /Zo_P => [] /functionsP. by move => [pa pd]; apply: Zo_i => //; apply /functionsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)