proposition: Lemma ex4_function_f_prop1 x a (y := ex4_function_fv a x): inc x ex4_F -> gle r a (ex4_fct_r x) -> inc y ex4_F /\ (ex4_fct_r y) = a.
proof: Proof. move => ha hb. move /ex4_inF_hi:(ha) => [h1 [h2 _ _ h5 h6 ] _]. move: (ex4_indexj_correct ha hb). set j:= (ex4_indexj x a); move => [ja jb jc]. set y1 := (restr x (csucc (ex4_indexj x a))). move: (NS_lt_nat ja h2) => jN. have lt1:csucc j <=c domain x by apply/(cleSltP jN). have pa: inc y1 ex4_F by apply:(ex4_F_stable_restr ha lt1); apply:succ_nz. have pb: ex4_fct_r y = a by rewrite/y -/y1; apply: ex4_modify_r_r. have pc: ex4_last y1 = j by rewrite /y1/ex4_last restr_d (cpred_pr2 jN). have pd: gle r a (ex4_fct_r y1). rewrite /ex4_fct_r pc /y1 -/j; rewrite LgV//; apply/(NltP (NS_succ jN)); fprops. split => //; apply:(ex4_F_stable_modify_r pa pd). rewrite pc => k lkj; rewrite /y1 -/j. have lkj': inc k (csucc j). by apply/(NltP (NS_succ jN)); move: (clt_leT lkj (cleS jN)). by rewrite LgV//; move => h; case:(cleNgt(jc _ (clt_ltT lkj ja) h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)