proposition: Lemma Exercise1_6f: bijection (two_projections_increasing r r' r'').
proof: Proof. move: (Exercise1_6e) (two_projections_fb E F G) => ra [fi fs]. have tpi:=(restriction2_fi fi ra). split; [ exact | split; first by fct_tac ]. move: ra => [ftp sstp sttp saux]. rewrite corresp_t => y yt. move: ((proj2 fs) _ (sttp _ yt)) => [x]; rewrite lf_source => xsf wx. suff xs1: (inc x (increasing_mappings r (order_product2 r' r''))). rewrite corresp_s; ex_tac; rewrite restriction2_V //. apply: Zo_i => //; first by rewrite order_product2_sr. move: (xsf) => /functionsP [fx sx tx]. move: (two_projections_aux fx sx tx) => [p1 p2 p3 p4 [p5 p6]]. split => //. apply: order_product2_or => //. rewrite order_product2_sr //. move=> u v uv; apply /order_product2_P. have us: (inc u E) by rewrite /E;order_tac. have vs: (inc v E) by rewrite /E;order_tac. rewrite -tx. move: (@two_projections_ax E F G) => t1. move: wx; rewrite /two_projections LfV // => aux. move:(f_equal P aux) (f_equal Q aux); aw => q1 q2. rewrite -(p5 _ us) -(p5 _ vs) -(p6 _ us) -(p6 _ vs) -q1 -q2. move: yt => /setX_P [_ ] /soimP [_ [_ _ _ ip]] /soimP [_ [_ _ _ iq]]. split;[ Wtac | Wtac | split; [ apply: (ip _ _ uv) | apply: (iq _ _ uv) ] ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)