proposition: Lemma ex4_indexj_idem x:inc x ex4_F -> ex4_indexj x (ex4_fct_r x) = ex4_last x.
proof: Proof. move => ha. move:(ex4_fct_r_in_I ha); set i:= (ex4_fct_r x); move => [iI _ _]. have leii: gle r i i by move:ex4H => [_ or sr _ _ ]; order_tac; rewrite sr. move:(ex4_indexj_correct ha leii) => [p1 p2 p3]. move: (ex4_length_prop1 ha) => [nN nv]. move /ex4_inF_hi: ha => [sa [q1 _ _ _ q5] _ ]. have la: (ex4_last x) <c domain x by apply: cpred_lt. move: p1; rewrite {1} nv; move/(cltSleP nN); case/cle_eqVlt => // lt. by case: (q5 _ _ lt la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)