proposition: Lemma Exercise1_24g r g: orsum_ax r g -> orsum_ax2 g -> anti_directed r -> let R := order_sum r g in exists X, [/\ sub X (substrate R), cofinal R X & anti_directed (induced_order R X)].
proof: Proof. move=> osa alne ar R. pose f i := J (rep (substrate (Vg g i))) i. have oR: order R by rewrite /R; fprops. have p1: forall i, inc i (domain g) -> inc (f i) (substrate R). move=> i idg; rewrite orsum_sr //; apply: disjoint_union_pi1=> //. apply: rep_i; apply: (alne _ idg). set X:= fun_image (domain g) f. have Xsr: sub X (substrate R). move=> t /funI_P [z zdf ->]; exact (p1 _ zdf). exists X; split => //. split => //x; rewrite orsum_sr //. Abort. Lemma nth_set11 K a (f:= nth_elt K)(g:= nth_elt (K +s1 a)) (q:= cardinal K) : sub K Nat -> finite_set K -> natp a -> (forall i, inc i K -> i <c a) -> (forall i, i<c q -> f i = g i) /\ g q = a. Proof. move => KN fsK aN Ha. have anK: ~ inc a K by move => /Ha []. move:(csucc_pr anK); set q1:= cardinal (K +s1 a);rewrite -/q => qv. have K1N: sub (K +s1 a) Nat by move => t /setU1_P; case; [apply: KN | move ->]. have qN: natp q by apply /NatP. have q1N: natp q1 by rewrite qv; fprops. move:(nth_set6 qN KN) (nth_set6 q1N K1N); rewrite -/q -/q1 qv => sa sb. suff aux: forall i, i<=c q -> nth_elts K i = nth_elts (K +s1 a) i. rewrite /f/g /nth_elt. split. move => i liq. move/(cleSltP (NS_lt_nat liq qN)): (liq) => /aux ->. by rewrite (aux _ (proj1 liq)). have hb: ((K +s1 a) -s K) = singleton a. apply:set1_pr; first by apply/setC_P; split; fprops. by move => z /setC_P [/setU1_P ha hb]; case: ha. by rewrite - (aux _ (cleR (CS_nat qN))) sb sa hb setU_1. move => i ilq; move:(NS_le_nat ilq qN) => iN. move: i iN ilq; apply: Nat_induction. by rewrite /nth_elts !induction_term0. move => n nN Hrec sc. rewrite (nth_elts_succ _ nN) (nth_elts_succ _ nN). have lenk:=(cleT (cleS nN) sc). rewrite - (Hrec lenk). move:(nth_set5 nN KN lenk) => [[]]. rewrite /nth_more; set S1 := (nth_elts K n) => ha hb hc. have s1: sub (K -s S1) Nat by move => t /setC_P [/KN]. have s2: sub ((K +s1 a) -s S1) Nat by move => t /setC_P [/K1N]. case:(emptyset_dichot (K -s S1)) => ne1. move:(cardinal_setC4 ha fsK); rewrite - /q hc ne1 cardinal_set0. by move: (nesym (cdiff_nz (clt_leT (cltS nN) sc))). have ne2: nonempty ((K +s1 a) -s S1). by exists a; apply/setC_P; split; [ fprops | move/ha]. move:(inf_Nat s1 ne1); set y1:= intersection _; move => [/setC_P[hu hv] pb]. move:(inf_Nat s2 ne2); set y2:= intersection _; move => [pa' pb']. apply: f_equal; apply:f_equal. have /pb' y21: inc y1 ((K +s1 a) -s S1) by apply/setC_P; split; fprops. move/setC_P:pa' => [/setU1_P hu1 hv1]; case: hu1=> hu1. by move/(setC_P): (conj hu1 hv1) => /pb le1; apply:cleA. by move:(Ha _ hu); rewrite - hu1 => /(cleNgt y21). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)