proposition: Lemma strict_increasing_compose3 f g h r r' r'' r''': strict_increasing_fun f r r' -> strict_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))) & strict_increasing_fun res r r'''].
proof: Proof. move=> sif sig sih. have icf:= (strict_increasing_w sif). have ich:= (strict_increasing_w sih). have ig:= (strict_increasing_w sig). have [chg Whg igh] := (increasing_compose ig ich). have [chgf Whgf ighf] := (increasing_compose icf igh). have aux x: inc x (source f) -> Vf ((h \co g) \co f) x = Vf h (Vf g (Vf f x)). move => xsf; rewrite !compfV //. move: (increasing_compose icf ig) => [[_ ff sgtf] _ _];Wtac. move=> res; rewrite /res;split => //. apply /functionsP; saw; fct_tac. move: ighf =>[qa qb qc qd]; split => // x y lxy. move: (arg1_sr (proj1 lxy)) (arg2_sr (proj1 lxy)). rewrite - (proj32 (proj43 sif)) => xsf ysf; rewrite !aux => //. by apply: (proj44 sih); apply: (proj44 sig); apply: (proj44 sif). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)