proposition: Lemma prl_r2_sf_prop3: prl_map2_compat prl_r2_sf S u.
proof: Proof. move:prl_r2_sf_prop1=> [vE vI vr vf]. move:(compat) => [cp1 cp2 cp3 cp4]; rewrite cp2 in cp3. split => //;first by rewrite vI vE; move => i iI; rewrite LgV//; apply: cp3. rewrite vf vr; move => i j lij. move: (prl_prop0 lij)=> [iI jI]. move:(cp3 _ iI) => [fu su tu]. by rewrite (cp4 _ _ lij) LgV// - su;apply: (compf_id_r fu). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)