proposition: Lemma isum_p11 f r r' g (fg := Lg (substrate r') (fun i => Vg f (Vf (inverse_fun g) i))): worder r -> order_isomorphism g r r' -> [/\ fgraph f, domain f = substrate r & allf f ordinalp] -> ipartial_sum f r (substrate r) = ipartial_sum fg r' (substrate r').
proof: Proof. move => wor isog axf. have rr: r \Is r' by exists g. have axg: [/\ fgraph fg, domain fg = substrate r' & allf fg ordinalp]. move: axf =>[qa qb qc]. rewrite /fg Lgd; split; fprops; hnf; aw => x xsr; rewrite LgV//; apply: qc. move: isog =>[_ _ /inverse_bij_bp [/proj1/proj1 bg sg tf] _]. rewrite qb; Wtac. move:(worder_invariance rr wor) => wor' {rr}. move: (isum_q2 wor axf (@sub_refl (substrate r))) => woa. move:(isum_q2 wor' axg (@sub_refl (substrate r'))) =>wob. move: (isum_q5 wor axf (@sub_refl (substrate r))) => sra. move: (isum_q5 wor' axg (@sub_refl (substrate r'))) => srb. rewrite 2! isum_p0; apply: (ordinal_o_isu1 woa wob). move: (proj1 woa) (proj1 wob) => oa ob. set A := disjointU (restr f (substrate r)). set B := disjointU (restr fg (substrate r')). pose h := (fun p => (J (P p) (Vf g (Q p)))). move: isog => [_ _ [bg sg th] gm]; move: (proj1 (proj1 bg)) => fctg. have axh: lf_axiom h A B. rewrite /h => x /isum_q6 [qa qb qc]; apply/isum_q6; aw. have ha: inc (Vf g (Q x)) (substrate r') by Wtac. split; fprops; rewrite /fg LgV//. rewrite (inverse_V2 bg) => //; ue. have bb: bijection (Lf h A B). apply: lf_bijective => //. move => u v /isum_q6 [qa qb qc] /isum_q6 [qa' qb' qc']. move/pr12_def => [sp sa]; apply: pair_exten => //. apply:(proj2 (proj1 bg)); ue. move => y /isum_q6 [qa qb qc]. have ytg: inc (Q y) (target g) by ue. move: (proj2 (proj2 bg) _ ytg); rewrite sg; move =>[x xsf xv]. exists (J (P y) x); last by rewrite /h; aw; rewrite - xv qc. apply/isum_q6; saw; fprops. move: qb; rewrite /fg LgV// xv inverse_V2 => //; ue. exists (Lf h A B). split => //; first by rewrite sra srb; saw. hnf; aw => x y xA yA. move:(axh _ xA) (axh _ yA) => xB yB. set H := (isum_q7 wor axf (@sub_refl (substrate r))). set H' := (isum_q7 wor' axg (@sub_refl (substrate r'))). have qxs: inc (Q x) (source g) by move/isum_q6: xA=> /proj31; ue. have qys: inc (Q y) (source g) by move/isum_q6: yA=> /proj31; ue. have ij: Vf g (Q x) = Vf g (Q y) -> Q x = Q y. by apply (proj2 (proj1 bg)). split. move/H => /proj33 etc; apply/H'; rewrite !LfV//; split => //. rewrite /h; aw; case: etc. move => [sa sb]; left; split; first by apply/(gm _ _ qxs qys). by move/ij. by move =>[sa sb]; right; rewrite sa. move/H' => /proj33 etc; apply/H; split => //. move: etc; rewrite /h !LfV//;aw; case. move => [/(gm _ _ qxs qys) sa sb];left. by split => // ss; case: sb; rewrite ss. move =>[/ij qa qb]; right; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)