proposition: Lemma EPfun_aux_M i j (h:= EPfun_aux): natp i -> natp j -> (glt r1 (Vf f i) (Vf f j) <-> glt r2 (Vf g (Vf h i)) (Vf g (Vf h j))).
proof: Proof. move => iN jN. move: (cmax_p1 (CS_nat iN) (CS_nat jN)). set n0 := cmax i j; move => [le1 le2]. have n0N: natp n0 by apply:Gmax_E. set n := csucc n0. have nN: natp n by apply/(NS_succ n0N). move: (cltS n0N); rewrite -/n => lnn. have lt1:= (cle_ltT le1 lnn). have lt2:=(cle_ltT le2 lnn). move:(EPfun_aux_pr2 nN) => [_ _ _ pd]. move: EPfun_aux_pr1 => [[qa _] qb qc _]. have i1: inc i n by apply /(NltP nN). have j1: inc j n by apply /(NltP nN). have qd: sub n (source EPfun_aux) by rewrite qb; apply: NS_inc_nat. by move: (pd i j lt1 lt2); rewrite restriction1_V // restriction1_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)