proposition: Lemma prl_map_inj S u F : prl_map_compat S u F -> (injection (projective_map S u F) <-> (forall y z, inc y F -> inc z F -> y <> z -> exists2 i, inc i (psI S) & (Vf (Vg u i) y <> Vf (Vg u i) z))).
proof: Proof. move => hb. move:(prl_map_prop hb) => [[fg sg tg]]. move: (prl_map_ax hb) => hu. split. move => [hc hd] y z yF zF yz; ex_middle bad; case:yz. rewrite sg in hd; apply: (hd y z yF zF); rewrite /projective_map/prl_map_val. rewrite !LfV//; apply: Lg_exten => i iS; ex_middle bad2; case: bad; ex_tac. move => h; split => //; rewrite sg => y z yF zF eq. case: (equal_or_not y z) => eyz//. move: (h _ _ yF zF eyz) => [i id]; case. move/(f_equal (Vg^~i)):eq. rewrite (projective_map_ev hb yF id). by rewrite (projective_map_ev hb zF id). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)