proposition: Lemma constant_fun_increasing f r r': order r -> order r' -> substrate r = source f -> substrate r' = target f -> constantfp f -> increasing_fun f r r' /\ decreasing_fun f r r'.
proof: Proof. move=> or or' sr sr' [ff cf]. split; split => // x y rxy; move:(arg1_sr rxy)(arg2_sr rxy); rewrite sr => xs ys; rewrite (cf _ _ xs ys); order_tac; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)