proposition: Lemma Exercise4_8qP X Y Z: sub X Z -> sub Y Z -> ((sub X Y) <-> (forall x, inc x Z -> gle E48Io (Vf (char_fun X Z) x) (Vf (char_fun Y Z) x))).
proof: Proof. move => XZ YZ; split. move => XY x xZ. apply / (Ninto_gleP2 NS0 NS1). case: (inc_or_not x X) => xX. rewrite (char_fun_V_a XZ xX) (char_fun_V_a YZ (XY _ xX)); split; fprops. have xc: inc x (Z -s X) by apply /setC_P. rewrite (char_fun_V_b XZ xc). case: (inc_or_not x Y) => xY. rewrite (char_fun_V_a YZ xY);split;fprops; apply:cle_01. have xc1: inc x (Z -s Y) by apply /setC_P. rewrite (char_fun_V_b YZ xc1); split;fprops; apply:cle_01. move=> h t tx; move: (h _ (XZ _ tx)). rewrite /E48Io; move /(Ninto_gleP) => [_ _ aux]; ex_middle ty. have tc: inc t (Z -s Y) by apply /setC_P;split => //; apply: XZ. move: aux; rewrite (char_fun_V_a XZ tx) (char_fun_V_b YZ tc). by move/(cltNge clt_01). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)