proposition: Lemma Exercise6_33u n: inc n N -> sub E6_33_Q (Vf X n).
proof: Proof. move => nN. move: (Exercise6_33t) => [qa qb qc qd]. rewrite / E6_33_Q - (qd _ nN) => t. have nn0: inc n N0 by apply: qb. move: (Exercise6_33r nn0) =>[sc qe qf]. move/functionsP: qe =>[fyr syr tyr]. move/(Imf_P fyr); rewrite syr; move =>[m ma ->]. rewrite - (qf _ ma) . move: Exercise6_33q =>[_ _ _] snc _. move: (Exercise6_33j (snc _ nn0)) => [sa sb <-]. move: sa =>[_ _ /proj31 byn _]. have fyn: function (y n) by fct_tac. Wtac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)