proposition: Lemma cnf_same_range: {when cnfp &, injective range}.
proof: Proof. move => x y ox oy sr. have sd: domain x = domain y by rewrite !cnf_card_range // sr. move:(ox) (oy) => [fgx nN hax hbx] [fgy _ hay hby]. apply:(fgraph_exten fgx fgy sd) => t tdz. move: (NS_inc_nat nN tdz) => tN; move: t tN tdz. apply: least_cardinal2 => i iN Hrec idx. have: inc (Vg y i) (range x) by rewrite sr; apply: (inc_V_range fgy); ue. move/(range_gP fgx) => [j jdx pv]. have jN:= (NS_inc_nat nN jdx). case: (NleT_ell jN iN) => lji; first by rewrite pv lji. move: (Hrec _ lji jdx); rewrite - pv => sv. rewrite sd in idx jdx. by rewrite pv (cnf_monomial_inj oy idx jdx (f_equal P sv)). move/(NltP nN): jdx => jdx. have ra: oexp x i <o oexp y i. move: (CNF_exponents_sM (proj42 ox) (proj1(proj44 ox)) lji jdx). by rewrite /oexp - pv. clear j jN pv lji jdx. have: inc (Vg x i) (range y) by rewrite - sr; apply: (inc_V_range fgx). move/(range_gP fgy) => [j jdx pv]. rewrite - sd in jdx. have jN:= (NS_inc_nat nN jdx). case: (NleT_ell jN iN) => lji; first by rewrite pv lji. move: (Hrec _ lji jdx); rewrite - pv => sv. by rewrite pv (cnf_monomial_inj ox jdx idx (f_equal P sv)). move/(NltP nN): jdx; rewrite sd => jdx. have rb: oexp y i <o oexp x i. move: (CNF_exponents_sM (proj42 oy) (proj1 (proj44 oy)) lji jdx). by rewrite /oexp - pv. case: (oltNge ra (proj1 rb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)