proposition: Lemma constant_increasing y: inc y F -> (inc (constant_function E F y) (increasing_mappings r r')).
proof: Proof. move => yF;move:(constant_prop E yF) => fp; apply /soimP; split => //. rewrite /E;split => // u v uv. rewrite (constant_V yF); last by order_tac. by rewrite (constant_V yF); order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)