proposition: Lemma isum_p3 n: inc n E -> ipartial_sum (singleton n) = Vg f n.
proof: Proof. move => nN. move:(fprop) => [hb hc hd]. have oi: ordinalp (Vg f n) by apply: hd; ue. move: (set1_1 n) => inn. rewrite isum_p0. have E1n: sub (singleton n) E by move => i /set1_P ->. have wo1 := (isum_q2 E1n). apply: ordinal_o_isu2 => //. set w := substrate (ipartial_order (singleton n)). have wP x: inc x w <-> [/\ Q x = n, inc (P x) (Vg f n) & pairp x]. rewrite /w (isum_q5 E1n); split. by move/ (isum_q6) =>[/set1_P ->]. move => [sa sb sc]; apply/isum_q6; rewrite sa; split; fprops. have ax1: lf_axiom P w (Vg f n) by move => t/wP []. exists (Lf P w (Vg f n)). move: (proj1 wo1) (proj1 (ordinal_o_wor oi))=> ov fon. split => //. rewrite ordinal_o_sr; saw; apply: lf_bijective => //. by move => x y /wP[ sa sb {2} <-] /wP [sd se {2} <-] ->; rewrite sa sd. move => y yi; exists (J y n); aw;trivial; apply/wP; aw; split; fprops. move => x y; rewrite lf_source => xw yw; rewrite !LfV //. move /wP: (xw) => [sa sn _]; move /wP: (yw) => [sc sd _]. split. move/(isum_q7 E1n x y)=>[_ _ ra]; apply/ordo_leP; split => //. by move: ra; rewrite sa sc; case; case => // _ /proj33. move/ordo_leP =>[_ _] h; apply/(isum_q7 E1n x y). rewrite - (isum_q5 E1n); split => //; rewrite sa sc; right; split => //. by split => //; apply:(Os_ordinal oi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)