proposition: Lemma Exercise1_6i f x: nonempty E -> nonempty F -> increasing_fun f (order_product2 r r') r'' -> inc x E -> increasing_fun (second_partial_fun G F f x) r' r''.
proof: Proof. move=> ne1 ne2 incf xsr. move: (Exercise1_6h ne1 ne2 incf) => [dsf rsf]. move: incf => [op or''' [ff sf tf] incf]. move: sf; rewrite order_product2_sr // => sf. have ax: inc f (functions (E \times F) G) by apply/functionsP. move: (spf_f ax xsr) => spf. split => //; [by split => //; rewrite /second_partial_fun; aw | move=> u v uv]. have us: (inc (J x u) (source f)). by rewrite sf; apply : setXp_i => //; order_tac. have vs: (inc (J x v) (source f)) by rewrite sf; apply : setXp_i => //; order_tac. have ur: inc u F by rewrite /F; order_tac. have vr: inc v F by rewrite /F; order_tac. rewrite (spf_V ax xsr ur) (spf_V ax xsr vr); apply: incf. by apply/order_product2_P; aw; rewrite - sf;split => //; split => //;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)