proposition: Lemma ex4_F_stable_modify_r x i: inc x ex4_F -> gle r i (ex4_fct_r x) -> (forall k, k <c (ex4_last x) -> ~ gle r i (P (Vg x k))) -> inc (ex4_modify_r x i) ex4_F.
proof: Proof. move => hx;move:(ex4_length_prop1 hx) => [sa sb]. move /ex4_inF_hi:hx => [h1 [h2 h3 _ h5 h6 ] h7] pa pc. set y := ex4_modify_r x i. have qq:ex4_last x <c domain x by rewrite sb; apply:cltS. have fgy: fgraph y by rewrite/y/ex4_modify_r; fprops. have dy: domain y = domain x by rewrite/y/ex4_modify_r; aw. have yl: Vg y (ex4_last x) = (J i (Q (Vg x (ex4_last x)))). by rewrite /y /ex4_modify_r; rewrite LgV//; [ Ytac0 | apply/(NltP h2) ]. have ynl j:j <c (domain x) -> j <> (ex4_last x) -> (Vg y j) = (Vg x j). by move => /(NltP h2)ha hb; rewrite/y /ex4_modify_r; rewrite LgV//; Ytac0. have qa j: j <c domain x -> pairp (Vg y j). move => jd; case: (equal_or_not j (ex4_last x)) => jl. rewrite jl yl; fprops. by rewrite ynl //; apply:h7. have or: order r by move:ex4H => []. apply:(ex4_inF h1 _ qa); split => //. move => j lij; move:(h5 _ lij) => ih5. case: (equal_or_not j (ex4_last x)) => jl; last by rewrite ynl. by rewrite jl yl; aw; apply: (leq_lt_trans or pa); rewrite/ex4_fct_r - jl. move => j k lkj ljm. have ljm': j <=c (ex4_last x) by apply/(cltSleP sa); rewrite - sb. rewrite (ynl _ (clt_ltT lkj ljm) (proj2 (clt_leT lkj ljm'))). case: (equal_or_not j (ex4_last x)) => jl. by rewrite jl yl; aw; apply: (pc k); rewrite - jl. by rewrite (ynl _ ljm jl); apply: h6. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)