proposition: Theorem decreasing_composition u v r r': decreasing_fun u r r' -> decreasing_fun v r' r -> (forall x, inc x (substrate r) -> gle r (Vf v (Vf u x)) x) -> (forall x', inc x' (substrate r') -> gle r' (Vf u (Vf v x')) x') -> (u \co v \co u = u /\ v \co u \co v = v).
proof: Proof. move=> [or or' [fu sr sr'] du] [_ _ [fv svr svr'] dv] h h'. have cvu: v \coP u by split => //; ue. have fvu: function (v \co u) by fct_tac. have cuv: u \coP v by split => //; ue. have fuv: function (u \co v) by fct_tac. have cuvu: (u \co v) \coP u by split => //; aw; ue. have cvuv: (v \co u) \coP v by split => //; aw; ue. split. apply: function_exten; aw; trivial;first by fct_tac. move=> x xs. rewrite sr in xs; move:(h _ xs)=> rel1; move: (du _ _ rel1)=> rel2. have p: inc (Vf u x)(substrate r') by rewrite - sr';Wtac. move: (h' _ p)=> rel3; rewrite !compfV //; try ue. order_tac. apply: function_exten; aw; trivial; first by fct_tac. move=> x xs. rewrite svr in xs; move:(h' _ xs)=> rel1; move: (dv _ _ rel1)=> rel2. have p: inc (Vf v x) (substrate r) by rewrite - svr';Wtac. move: (h _ p)=> rel3; rewrite !compfV //; try ue. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)