proposition: Lemma increasing_compose f g r r' r'': increasing_fun f r r' -> increasing_fun g r' r'' -> [/\ g \coP f, (forall x, inc x (source f) -> Vf (g \co f) x = Vf g (Vf f x)) & increasing_fun (g \co f) r r''].
proof: Proof. move=> [or or' [ff sf tf] icf][_ or'' [fg sg tg] icg]. have cgf: (g \coP f) by split => //; ue. have p:(forall x, inc x (source f) -> Vf (g \co f) x = Vf g (Vf f x)). move=> x xsf; rewrite compfV//. split => //; split => //; first by saw; fct_tac. move => x y xy. have xsf: inc x (source f) by rewrite sf; order_tac. have ysf: inc y (source f) by rewrite sf; order_tac. by rewrite p // p //; apply: icg; apply: icf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)