proposition: Lemma bn_nn: bijection_prop function_n2_n (coarse Nat) Nat.
proof: Proof. move: value_bij => [bv sv tv]. have ax0 := value_nat. have ax1 x: natp x -> inc (Vf (inverse_fun valuef) x) dexpansions. move => xn; rewrite - sv; apply: inverse_Vis => //; ue. have ax2 p: inc p (coarse Nat) ->inc (wedge (Vf (inverse_fun valuef) (P p)) (Vf (inverse_fun valuef) (Q p))) dexpansions. by move => /setX_P [pp pa pb]; apply: wedge_exp; apply: ax1. rewrite /function_n2_n; saw; apply: lf_bijective. - by move => p pp; apply: ax0; apply: ax2. - move => u v uc vc; move/(value_inj (ax2 _ uc) (ax2 _ vc)) => sv1. move/setX_P: uc =>[pa pb pc];move/setX_P: vc =>[pd pe pf]. move: (ax1 _ pb) (ax1 _ pc) (ax1 _ pe) (ax1 _ pf) => qa qb qc qd. move:(wedge_i1p qa qb) (wedge_i1p qc qd); rewrite sv1 => -> eqa. move:(wedge_i2p qa qb) (wedge_i2p qc qd); rewrite sv1 => -> eqb. move:(f_equal (Vf valuef) eqa); rewrite inverse_V ? inverse_V //; try ue. move:(f_equal (Vf valuef) eqb); rewrite inverse_V ? inverse_V //; try ue. by move => ra rb; apply: pair_exten. - move => y yN; have ytc: inc y (target valuef) by ue. move: (inverse_V bv ytc) (inverse_Vis bv ytc). set x := (Vf (inverse_fun valuef) y) =>[qa qb]. move: qb; rewrite {1} /valuef; aw => xd. move: qa; rewrite {1} /value LfV// => vx. move: (wedge_inverse xd). set x1 := (wedge_i1 x); set x2 := (wedge_i2 x). move =>[x1p x2p x12]. move:(wedge_i1p x1p x2p) (wedge_i2p x1p x2p) (wedge_exp x1p x2p). set x3 := wedge x1 x2; move => x3a x3b x3t. have x1v: (Vf (inverse_fun valuef) (value x1)) = x1. have ->: value x1 = Vf valuef x1 by rewrite /valuef LfV. by apply: (inverse_V2 bv); ue. have x2v: (Vf (inverse_fun valuef) (value x2)) = x2. have ->: value x2 = Vf valuef x2 by rewrite /valuef LfV. by apply: (inverse_V2 bv); ue. set z := J (value x1) (value x2). exists z; first by apply:setXp_i; apply: ax0. by rewrite /z; aw; rewrite {1} x1v x2v x12. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)