proposition: Lemma increasing_compose3 f g h r r' r'' r''': strict_increasing_fun f r r' -> increasing_fun g r' r'' -> strict_increasing_fun h r'' r''' -> let res:= (h \co g) \co f in [/\ inc res (functions (source f) (target h)), (forall x, inc x (source f) -> Vf res x = Vf h (Vf g(Vf f x))) & increasing_fun res r r'''].
proof: Proof. move=> sif ig sih. have icf:= (strict_increasing_w sif). have ich:= (strict_increasing_w sih). have [chg Whg igh] := (increasing_compose ig ich). have [chgf Whgf ighf] := (increasing_compose icf igh). move=> res; rewrite /res;split => //. apply /functionsP; saw; fct_tac. move=> x xsf; rewrite ! compfV//. move: (increasing_compose icf ig) => [[_ ff sgtf] _ _];Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)