proposition: Lemma Exercise1_6j f: nonempty E -> nonempty F -> increasing_fun f (order_product2 r r') r'' -> (restriction2_axioms (second_partial_function G E F f) E (increasing_mappings r' r'')).
proof: Proof. move=> ne1 ne2 incf. move: (Exercise1_6h ne1 ne2 incf) => [dsf rsf]. move: (incf) => [op or''' [ff sf tf] icf]. move: sf; rewrite order_product2_sr // => sf. have ax: inc f (functions (E \times F) G) by apply/functionsP. move: (spfa_f ax) => spfa. split => //. rewrite lf_source; fprops. rewrite lf_target; apply:Zo_S. have aa: sub E (source (second_partial_function G E F f)). rewrite lf_source; fprops. move=> t /(Vf_image_P spfa aa) [x xsr ->]. move: (Exercise1_6i ne1 ne2 incf xsr) => h. move: (spf_f ax xsr) => spf. rewrite (LfV (spfa_axiom ax) xsr); apply /soimP; split => //. by hnf; rewrite lf_source lf_target. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)