proposition: Lemma osum_set1 r g i: order_on r (domain g) -> substrate r = singleton i -> ordinalp (Vg g i) -> osum r g = Vg g i.
proof: Proof. move=> [or sr] srs otve. have dgi: domain g = singleton i by rewrite - sr srs. have idg: inc i (domain g) by rewrite dgi; fprops. have wor:= (worder_set1 (conj or srs)). have ove:= (ordinal_o_wor otve). rewrite /osum /Lgcomp. set g' := Lg _ _. have osa: orsum_ax r g'. rewrite /g'; hnf; saw => //;hnf; aw. rewrite dgi => j /set1_P ->; rewrite LgV// ; fprops. have wos: worder (order_sum r g'). rewrite/g';apply: orsum_wor; first by saw. hnf; rewrite Lgd dgi; move=> j /set1_P ->; rewrite LgV //; fprops. apply: (ordinal_o_isu2 wos otve). set (E:= substrate (order_sum r g')); set (F := substrate (ordinal_o (Vg g i))). have He:E =sum_of_substrates g' by rewrite /E orsum_sr //. have Hf:F = Vg g i by apply: (ordinal_o_sr). have uE: (forall u, inc u E <-> [/\ pairp u, Q u = i &inc (P u) F]). move=> u; rewrite He /g'; split. move=> us; move: (du_index_pr1 us) => []. rewrite Lgd; move=> Qu; rewrite LgV //. move: Qu; rewrite dgi=> /set1_P -> pa pb; split => //; ue. move => [pu Qu Pu]; rewrite - pu Qu; apply: disjointU_pi; aw; trivial. by rewrite ! LgV//; aw. have ta: (lf_axiom P E F) by move=> t /uE [_]. exists (Lf P E F). split; fprops; first (hnf;saw). apply: lf_bijective => //. move=> u v =>/uE [pu Qu Pu] /uE [pv Qv Pv] sp. apply: pair_exten =>//; ue. move=> y ys; exists (J y i); aw => //; apply /uE; saw;fprops. hnf; aw => a b aE bE; rewrite !LfV //. move: (aE)(bE) => /uE [pu Qu Pu] /uE [pv Qv Pv]. have aux: inc (Q a) (domain g) by rewrite dgi Qu ; fprops. have <-: (Vg g' (Q a)) = ordinal_o (Vg g i) by rewrite /g' LgV// Qu. split. by move /orsum_gleP => [_ _]; case; move => [_] //; rewrite Qu Qv. move => h; apply /orsum_gleP;split; rewrite - ? He //; right;split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)