proposition: Lemma Exercise1_6d f: increasing_fun f r (order_product2 r' r'') -> (increasing_fun (first_projection f E F) r r' /\ increasing_fun (secnd_projection f E G) r r'').
proof: Proof. move=> [_ op [ff sr sor] icf]. rewrite order_product2_sr // in sor. move: (two_projections_aux ff sr sor) => [taP taQ fP fQ [WP WQ]]. rewrite /E/increasing_fun /first_projection/secnd_projection; split. split => //;[saw | move=> x y xy; rewrite !LfV//; try order_tac]. by move: (icf _ _ xy) => /order_product2_P [_ _ ][]. split => //; [saw | move=> x y xy; rewrite !LfV//; try order_tac]. by move: (icf _ _ xy) => /order_product2_P [_ _ ][]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)