proposition: Lemma OTsum_set1 r g i: order_on r (domain g) -> domain g = singleton i -> order_type (Vg g i) -> OT_sum r g = Vg g i.
proof: Proof. move=> [or sr] dgi otve. have idg: inc i (domain g) by rewrite dgi; fprops. have eqa:= (OT_prop5 otve). have or1:= (OT_prop2 otve). rewrite /OT_sum. set g1 := Lg (domain g) (fun z => Vg g i). have ->: Lg (domain g) (fun z => order_type_of (Vg g z)) = g1. by apply: Lg_exten => k kdg; aw; move:kdg; rewrite dgi => /set1_P ->. suff: (order_sum r g1) \Is Vg g i. by move => /order_type_unique; rewrite (OT_prop5 otve). have osa: orsum_ax r g1. rewrite /g1. hnf; aw;split => //; hnf; aw => x xdg; rewrite LgV//. set (E:= substrate (order_sum r g1)); set (F := substrate (Vg g i)). have He:E = sum_of_substrates g1 by rewrite /E orsum_sr //. have uE: (forall u, inc u E <-> [/\ pairp u, Q u = i &inc (P u) F]). move=> u; rewrite He /g1; 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. rewrite LgV// ; aw; trivial;rewrite LgV//. 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; aw;split;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 Qu dgi; fprops. split. move /orsum_gleP => [_ _]; rewrite/order_sum_r Qu Qv; case; case => //. rewrite /g1 LgV//. move => h; apply /orsum_gleP;hnf; rewrite - He /order_sum_r /g1 LgV//. by split => //; rewrite Qu Qv; right. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)