proposition: Lemma Exercise1_6e: (restriction2_axioms (two_projections E F G) (increasing_mappings r (order_product2 r' r'')) ((increasing_mappings r r') \times (increasing_mappings r r''))).
proof: Proof. move: (two_projections_fb E F G) (@two_projections_ax E F G) => bt t1. split => //. + fct_tac. + rewrite lf_source /increasing_mappings order_product2_sr //;apply: Zo_S. + rewrite lf_target; apply: setX_Slr; apply: Zo_S. + move: (bij_function bt) => ff. have pa: (sub (increasing_mappings r (order_product2 r' r'')) (source (two_projections E F G))). by move => t; rewrite lf_source => /Zo_S; rewrite order_product2_sr. move=> t /(Vf_image_P ff pa) [u /Zo_P []]. rewrite order_product2_sr // => aux. move: (aux) => /functionsP [fu su tu]. move: (two_projections_aux fu su tu) => [_ _ p1 p2 _] uinc. move: (Exercise1_6d uinc) => [i1 i2] ->. by rewrite - /two_projections LfV //; apply: setXp_i => //; apply : Zo_i => //; apply /functionsP; hnf; rewrite lf_source lf_target. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)