proposition: Lemma ex4_function_f_id a: inc a I -> (ex4_function_f (J a a)) = identity (ex4_setEi a).
proof: Proof. move => aI. move:(ex4H) => [_ or sr _ _]. have leaa: gle r a a by order_tac; rewrite sr. move:(ex4_function_f_fun leaa) (ex4_function_f_ax leaa) => [pa pb pc] ax. apply: function_exten; aww; rewrite pb => x xp. rewrite /ex4_function_f (idV xp); aw; rewrite LfV//. rewrite / ex4_function_fv. move/Zo_P: xp => [xf xv]. move: (ex4_length_prop1 xf) => [nN nv]. move: (ex4_indexj_idem xf); rewrite xv => eq; rewrite eq - nv /restr. move:(ex4_inF_hi xf) => [_[h1 h2 _ _ _ ]] h3. rewrite (Lg_recovers h2) / ex4_modify_r; apply:fgraph_exten; aww. move => i idx /=; rewrite LgV//; Ytac eq1 => //; rewrite - xv. by rewrite /ex4_fct_r - eq1 h3 //; apply/(NltP h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)