proposition: Lemma Exercise5_9k2 n q k J (e := nth_elt J): natp k -> Ex59_Jprop q n k J -> [/\ forall x y, x <c y -> y <c k -> e x <c e y, forall x y, x <=c y -> y <c k -> e x <=c e y, forall x y, x <c k -> y <c k -> e x = e y -> x = y, forall x, x <c k -> inc (e x) J & forall y, inc y J -> exists2 i, i <c k & y = e i].
proof: Proof. move => kN [ sa sb _ _]. have ra:forall x y, x <c y -> y <c k -> e x <c e y. move => x y lxy lyk. by apply: (nth_elt_monotone (NS_lt_nat lyk kN) sb) lxy; rewrite sa. have rc:forall x, x <c k -> inc (e x) J. by move => x lxk; apply: (nth_elt_inK (NS_lt_nat lxk kN) sb); rewrite sa. split => //. + move => x y ha hb; case: (equal_or_not x y). by move => ->; apply/cleR/CS_nat/sb/rc. move => nxy; exact (proj1(ra _ _ (conj ha nxy) hb)). + move => x y lxk lyk exy; case: (cleT_ell (proj31_1 lxk) (proj31_1 lyk)) => //. - by move => lxy; case: (proj2 (ra _ _ lxy lyk)). - by move => lxy; case: (proj2 (ra _ _ lxy lxk)). + move => y yJ. rewrite - sa in kN. by move:(nth_elt_surj sb kN yJ) => [x]; rewrite sa => xa xb; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)