proposition: Lemma ns_extensions_prop4 (swap0 := variant C0 C1 C0) (swap1 := fun x => (J (P x) (swap0 (Q x)))) (swap2 := fun x => (fun_image x swap1)) (swap3 := fun x => fun_image x (fun z => J (swap1 (P z))(swap1 (Q z)))) (r3 := order_sum2 rB rA): r3 \Is swap3 r3 /\ inc (swap3 r3) ns_extensions.
proof: Proof. move: wor1 wor2 =>[wo1 sr1][wo2 sr2]. move: (orsum2_wor wo2 wo1) => wor3. move: (orsum2_sr (proj1 wo2) (proj1 wo1)) ; rewrite sr1 sr2=> sr4. pose C' := canonical_du2 B A. move: C1_ne_C0 C0_ne_C1 => c01 c10. have eq1: swap2 C' = C. set_extens t. move=> /funI_P [z /candu2P [pa pb] ->]; apply/candu2P. rewrite/swap1;aw; split; first fprops. case: pb. by move =>[pc ->]; right; split => //; rewrite /swap0 variant_true. by move =>[pc ->]; left; split => //; rewrite /swap0 variant_false. move/candu2P => [pp]; case. move=>[pa pb]; apply/funI_P. exists (J (P t) C1); first by apply:candu2_prb. by rewrite /swap1/swap0; aw; rewrite -pb pp. move=>[pa pb]; apply/funI_P. exists (J (P t) C0); first by apply:candu2_pra. by rewrite /swap1/swap0; aw; rewrite -pb pp. pose f := Lf swap1 C' C. have sf: source f = C' by rewrite /f; aw. have tf : target f = C by rewrite /f; aw. have ax0: lf_axiom swap1 C' C. by rewrite - eq1; move => t rx; apply/funI_P; ex_tac. have bf: bijection f. rewrite /f - eq1; apply: lf_bijective. - move => t rx; apply/funI_P; ex_tac. - move => u v /candu2P [pp1 pu] /candu2P [pp2 pv] eq2. move: (pr1_def eq2) (pr2_def eq2) => eq3 eq4. apply: pair_exten => //; move: eq4; rewrite/swap0. case: pu; case: pv ;move => [_ ->] [_ ->] //. by rewrite (variant_false _ _ c01) variant_true. by rewrite (variant_false _ _ c01) variant_true. - move => y /funI_P [z zC ->]; ex_tac. have eq2 : Vfs (f \ftimes f) r3 = (swap3 r3). have ff := proj1 (proj1 bf). have fff := ext_to_prod_f ff ff. have sff: source (f \ftimes f ) = coarse C' by rewrite /ext_to_prod sf; aw. have ss: sub r3 (source (f \ftimes f)). rewrite sff /C' - sr4; apply sub_graph_coarse_substrate. exact (proj41 (proj1 wor3)). have ax: lf_axiom (fun z => J (Vf f (P z)) (Vf f (Q z))) (source f \times source f) (target f \times target f). by move => t /setX_P [pt ha hb]; apply: setXp_i; Wtac. set_extens t. move/(Vf_image_P fff ss) => [u ur3 ->]. move: (ss _ ur3); rewrite sff - sf => ucf. move/setX_P: (ucf); rewrite sf; move => [_ p1c p2c]. rewrite /ext_to_prod; aw; rewrite/swap3/f !LfV//. apply/funI_P; ex_tac. move=>/funI_P [z zr3 -> ]; apply/(Vf_image_P fff ss); ex_tac. move: (ss _ zr3); rewrite sff - sf => ucf. move/setX_P: (ucf); rewrite sf; move => [_ p1c p2c]. by rewrite /ext_to_prod; aw; rewrite/swap3/f ! LfV. have sf': substrate (order_sum2 rB rA) = source f by rewrite /f; aw. move:(order_transportation bf (conj (proj1 wor3) sf')); rewrite eq2 => oif. have is1: r3 \Is swap3 r3 by exists f. have sr3: substrate (swap3 r3) = C. by move: (proj33 (proj43 oif)); rewrite tf. move: (worder_invariance is1 wor3)=> wor4. split => //; apply/ns_extensions_prop1; split => //. move => t /Zo_P [/setX_P[qa qb qc] qd]; rewrite - qa; apply/funI_P. move/candu2P: qb => [sa sb]. move/candu2P: qc => [sa' sb']. case: qd. move => [ha hb hc]. exists (J (J (P (P t)) C1) (J (P (Q t)) C1)). apply /orsum2_gleP. rewrite sr1 sr2; split. - by apply: candu2_prb; case: sb; case => //; rewrite ha. - by apply: candu2_prb; case: sb'; case => //; rewrite hb. - by constructor 2; aw. by rewrite /swap1/swap0; aw; rewrite - {1} ha sa - hb sa'. move => [ha hb hc]. case: sb; [ by move => [_ bb]; case: ha | move => [ra rb]]. case: sb'; [ by move => [_ bb]; case: hb | move => [ra' rb']]. exists (J (J (P (P t)) C0) (J (P (Q t)) C0)). apply /orsum2_gleP; rewrite sr1 sr2; split. - by apply: candu2_pra. - by apply: candu2_pra. - by constructor 1; aw. by rewrite /swap1/swap0; aw; rewrite - {1} rb sa -rb' sa'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)