proposition: Lemma functions_incr_inv r1 r2 r3 r4: r1 \Is r3 -> r2 \Is r4 -> (functions_incr r1 r2) =c (functions_incr r3 r4).
proof: Proof. move => [f isf] [g isg]. have isif:= (inverse_order_is isf). have isig:= (inverse_order_is isg). pose Phi h := (g \co h) \co inverse_fun f. move: (order_isomorphism_increasing isif) => ifsi. move: (order_isomorphism_increasing isg) => gsi. move: (order_isomorphism_increasing isf) => fsi. move: (order_isomorphism_increasing isig) => igsi. move: (proj43 isf) => [bf sf tf]. move: (proj43 isg) => [bg sg tg]. have fg: function g by fct_tac. set S := (functions_incr r1 r2); set T := (functions_incr r3 r4). have ax: lf_axiom Phi S T. rewrite /Phi => t; move/Zo_hi => qa. move: (increasing_compose3 ifsi qa gsi) =>[qb _ qc]. by apply: Zo_i => //; move: qb; aw; rewrite tf tg. apply/card_eqP; exists (Lf Phi S T); saw; apply: lf_bijective => //. move => u v /Zo_S /functionsP [fu su tu] /Zo_S /functionsP [fv sv tv]. move: (proj31 (proj43 isif)) => qa. have co3: g \coP u by split => //; ue. have co4: g \coP v by split => //; ue. have co1: (g \co u) \coP inverse_fun f. split => //; try fct_tac; aw; ue. have co2: (g \co v) \coP inverse_fun f. split => //; try fct_tac; aw; ue. by move/ (compf_regl qa co1 co2); move/ (compf_regr bg co3 co4). move => k /Zo_P [/functionsP [fk sk tk] mk]. move: (increasing_compose3 fsi mk igsi) =>[rb _ rc]. exists ((inverse_fun g \co k) \co f). by apply:Zo_i => //; apply/functionsP; exact: (proj43 rc). have ma: k \coP f by move: (proj31 (proj43 fsi)) =>ff; split => //; ue. have mb: inverse_fun g \coP k by split=>//; aw; try ue; apply: bijective_inv_f. have mc: function (k \co f) by fct_tac. have md: target g = target (k \co f) by aw; ue. rewrite /Phi - (compfA mb ma) (compf_lK' bg mc md) (compf_rK) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)