proposition: Lemma CR_prop12: injection (Lf CR_limit CR_set BR).
proof: Proof. apply: lf_injective; first by apply:CR_prop11. move => u v uI vI sm; ex_middle nuv. set E := Zo Nat (fun i => (Vf u i <> Vf v i)). case:(emptyset_dichot E) => ee. move/functionsP:uI=> [fu su tu]; move/functionsP:vI => [fv sv tv]. apply :(function_exten fu fv); [ ue | ue | ]. rewrite su;move => n nN /=; ex_middle bad. empty_tac1 n; apply/Zo_P; split => //. have sEN: sub E Nat by apply: Zo_S. move:(inf_Nat sEN ee) ; set k := intersection E; move => [kq kp]. have kN := sEN _ kq. have lkp: forall i, i <c k -> Vf u i = Vf v i. move => i lik; ex_middle bad; case: (cltNge lik); apply: kp; apply:Zo_i => //. apply: (NS_lt_nat lik kN). have lkk: Vf u k <> Vf v k by case /Zo_P: kq. have: CR_partial_sum u k = CR_partial_sum v k +q (CR_inv3n k) \/ CR_partial_sum v k = CR_partial_sum u k +q (CR_inv3n k). rewrite /CR_partial_sum (qsum_rec _ kN) (qsum_rec _ kN). set x := qsum _ _; set y := qsum _ _. have <-: x = y. have aux: forall n, natp n -> n <=c k -> qsum (CR_next_term u) n = qsum (CR_next_term v) n. apply:Nat_induction; first by rewrite !qsum0. move => n nN Hrec snk. rewrite (qsum_rec _ nN) (qsum_rec _ nN). move/(cleSltP nN): snk => lnk. by rewrite (Hrec (proj1 lnk)); rewrite /CR_next_term (lkp _ lnk). exact:(aux k kN (cleR (CS_nat kN))). have xq: ratp x by exact:(BQp_sBQ(CR_prop4 uI kN)). move/functionsP:uI => [fu su tu];move/functionsP:vI => [fv sv tv]. rewrite /CR_next_term; set w := CR_inv3n k. have uk2: (Vf u k) = \0c \/ (Vf u k) = \1c. by apply/set2_P; rewrite - [doubleton _ _]/ \2c; Wtac; rewrite su. have vk2: (Vf v k) = \0c \/ (Vf v k) = \1c. by apply/set2_P; rewrite - [doubleton _ _]/ \2c; Wtac; rewrite sv. have wq: ratp w. apply: (CR_prop1 kN). move:lkk;case: uk2 => uk; rewrite uk;case: vk2 => vk; rewrite vk. + by case. + by right ;rewrite (BQprod_0l wq) (BQprod_1l wq)(BQsum_0l xq) BQsumC. + by left;rewrite (BQprod_0l wq) (BQprod_1l wq)(BQsum_0l xq) BQsumC. + by case. case => H. by case:(CR_prop10 uI kN);move: (CR_prop9 vI kN); rewrite - H - sm. by case:(CR_prop10 vI kN); move: (CR_prop9 uI kN); rewrite - H - sm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)