proposition: Lemma ex4_fct_r_in_I x: inc x ex4_F -> [/\ inc (ex4_fct_r x) I, inc (ex4_fct_s x) I & glt r (ex4_fct_r x) (ex4_fct_s x)].
proof: Proof. move => hx; move:(ex4_length_prop1 hx) => [sa sb]. move:(ex4_inF_hi hx) => [p1 [pa pb pc pd pe] p2]. have qq:ex4_last x <c domain x by rewrite sb; apply:cltS. by move: (pd _ qq) => lt; move:(ex4_or_prop0 (proj1 lt)) => [iI jI]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)