proposition: Lemma Exercise1_6k: nonempty E -> nonempty F -> lf_axiom (fun f=> restriction2 (second_partial_function G E F f) E (increasing_mappings r' r'')) (increasing_mappings (order_product2 r r') r'') (increasing_mappings r (increasing_mappings_order r' r'')).
proof: Proof. move=> ne1 ne2. have o1: order (order_product2 r r') by apply: order_product2_or. move: (imo_osr r' or'') => [o2 sr2]. move=> t /soimP [[ft st tt] int]. move: (Exercise1_6j ne1 ne2 int) => ra. move: (Exercise1_6h ne1 ne2 int) => [dst rst]. move: st; rewrite order_product2_sr // => st. have ax: inc t (functions (E \times F) G) by apply/functionsP. set g:= restriction2 _ _ _. have fg: function g by rewrite /g; apply: (proj31(restriction2_prop ra)). have sg: source g = E by rewrite /g /restriction2; aw. have tg: target g = substrate (increasing_mappings_order r' r''). by rewrite sr2 /g /restriction2; aw. apply /soimP; split => //; split => //. move => x y xy. have xsr: (inc x E) by rewrite /E; order_tac. have ysr: (inc y E) by rewrite /E; order_tac. rewrite /g restriction2_V // restriction2_V // spfa_V // spfa_V //. apply /imo_gleP => //. move:(Exercise1_6i ne1 ne2 int xsr)(Exercise1_6i ne1 ne2 int ysr). move=> inc1 inc2; move: (inc1)(inc2). move => [_ _ [fsx ssx tsx] isx] [_ _ [fsy ssy tsy] isy]. split; [ by apply /soimP | by apply /soimP | split => //]. move => i isr; rewrite (spf_V ax xsr isr); rewrite (spf_V ax ysr isr). have Js: (inc (J x i) (source t)) by rewrite st; apply /setXp_i. have Js': (inc (J y i) (source t)) by rewrite st; apply /setXp_i. apply: (proj44 int). apply /order_product2_P;saw; try apply /setXp_i => //. split => //; order_tac => //;ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)