proposition: Lemma ex4_indexj_correct x a (j := ex4_indexj x a): inc x ex4_F -> gle r a (ex4_fct_r x) -> [/\ j <c (domain x), gle r a (P (Vg x j)) & forall k, k <c (domain x) -> gle r a (P (Vg x k)) -> j <=c k].
proof: Proof. move => ha hb. rewrite /j /ex4_indexj; set U := Zo _ _. move: (ex4_length_prop1 ha); set n := domain x; move => [xa xb]. have nN: natp n by rewrite xb; apply: NS_succ. have csu: cardinal_set U. move => t /Zo_P [ h _]; exact:(CS_nat (NS_inc_nat nN h)). have neu: nonempty U. exists (cpred n); apply /Zo_P; split => //. by apply/(NltP nN); rewrite {2} xb; apply: (cltS xa). move: (cle_wor' csu neu); set u := intersection U; move => [ua ub]. move/Zo_P: ua => [ /(NltP nN) ra rb]; split => // k lkn h. by apply: ub; apply/Zo_P; split => //; apply/(NltP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)