proposition: Lemma FinCompact_correct : forall x (s:FinEnum (Complete X)), InFinEnumC x s <-> inCompact x (FinCompact s).
proof: Proof. intros x s. split. intros H e1 e2. simpl. induction s. exfalso; exact (FinSubset_ball_nil H). move H after IHs. apply FinSubset_ball_orC in H. destruct H as [G | H | H] using orC_ind. intro abs; contradict G; intro G; contradiction. intro abs; contradict abs. exists (approximate a e2). split. left. reflexivity. specialize (H e1 e2). rewrite Qplus_0_r in H. exact H. apply FinSubset_ball_cons. apply IHs; auto. intros H. induction s. exfalso; exact (FinSubset_ball_nil (H (1#1) (1#1))%Qpos). unfold inCompact in H. simpl in H. set (P:= fun n (b:bool) => if b then (let e1 := (1#P_of_succ_nat n)%Qpos in let e2 := e1 in (ball (m:=X) (proj1_sig e1 + proj1_sig e2) (approximate x (Qpos2QposInf e1)) (approximate a (Qpos2QposInf e2)))) else (let e1 := (1#P_of_succ_nat n)%Qpos in let e2 := e1 in (FinSubset_ball (proj1_sig e1 + proj1_sig e2) (approximate x (Qpos2QposInf e1)) (FinCompact_raw s (Qpos2QposInf e2))))). assert (L: (forall n : nat, existsC bool (fun x => ~ ~ In x (true :: false :: nil) /\ P n x))). { intros n. specialize (H (1#P_of_succ_nat n)%Qpos (1#P_of_succ_nat n)%Qpos). apply FinSubset_ball_orC in H. destruct H as [ G | L | L] using orC_ind. auto using existsC_stable. apply existsWeaken. exists true. split; auto with *. apply existsWeaken. exists false. split; auto with *. } destruct (infinitePidgeonHolePrinicple _ _ _ L) as [G | c [_ Hc]] using existsC_ind. intro abs. contradict G; intro G. contradiction. destruct c. - intro abs; contradict abs. exists a. split. left. reflexivity. unfold P in Hc. apply ball_eq. intros e epos. destruct (((1#4)*exist _ _ epos)%Qpos) as [[en ed] He] eqn:des. destruct en as [|en|en]. inversion He. 2: inversion He. simpl in He. destruct (Hc (pred (nat_of_P ed))) as [G | m [Hm0 Hm1]] using existsC_ind. apply (msp_stable (msp _)), G. set (m' := (1#P_of_succ_nat m)%Qpos). apply ball_weak_le with (proj1_sig (m' + (m' + m') + m')%Qpos). unfold m'. simpl. setoid_replace ((1 # Pos.of_succ_nat m) + ((1 # Pos.of_succ_nat m) + (1 # Pos.of_succ_nat m)) + (1 # Pos.of_succ_nat m)) with ((1#P_of_succ_nat m)/(1#4)) by (simpl; field). apply Qle_shift_div_r. reflexivity. rewrite -> Qmult_comm. setoid_replace ((1#4)*e) with (proj1_sig ((1#4)*exist _ _ epos)%Qpos) by reflexivity. rewrite des. unfold Qle; simpl. rewrite Zpos_mult_morphism. apply Z.le_trans with (Z.pos en * Z.pos ed)%Z. rewrite Z.mul_comm, <- Z.le_mul_diag_r. apply Pos.le_1_l. reflexivity. apply Zmult_le_compat_l. 2: discriminate. rewrite Pos.of_nat_succ. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite <- (Nat.lt_succ_pred O _). apply le_n_S. exact Hm0. apply Pos2Nat.is_pos. discriminate. eapply ball_triangle;[|apply ball_approx_l]. eapply ball_triangle;[apply ball_approx_r|]. rewrite -> ball_Cunit. apply Hm1. - apply FinSubset_ball_cons. apply IHs. unfold P in Hc. intros e1 e2. apply FinSubset_ball_closed. intros d dpos. destruct (((1#4)*exist _ _ dpos)%Qpos) as [[dn dd] Hd] eqn:des. destruct dn as [|dn|dn]. inversion Hd. 2: inversion Hd. destruct (Hc (pred (nat_of_P dd))) as [G | m [Hm0 Hm1]] using existsC_ind. intro abs; contradict G; intro G; contradiction. set (m' := (1#P_of_succ_nat m)%Qpos). apply FinSubset_ball_weak_le with (proj1_sig ((e1 + m') + (m' + m') + (m' + e2))%Qpos). simpl. rewrite -> Qle_minus_iff. setoid_replace ( proj1_sig e1 + proj1_sig e2 + d + - (proj1_sig e1 + (1 # Pos.of_succ_nat m) + ((1 # Pos.of_succ_nat m) + (1 # Pos.of_succ_nat m)) + ((1 # Pos.of_succ_nat m) + proj1_sig e2))) with (d + - (proj1_sig m' + (proj1_sig m' + proj1_sig m') + proj1_sig m')) by (simpl; ring). rewrite <- Qle_minus_iff. unfold m'. autorewrite with QposElim. setoid_replace (proj1_sig (1 # Pos.of_succ_nat m)%Qpos + (proj1_sig (1 # Pos.of_succ_nat m)%Qpos + proj1_sig (1 # Pos.of_succ_nat m)%Qpos) + proj1_sig (1 # Pos.of_succ_nat m)%Qpos) with ((1#P_of_succ_nat m)/(1#4)) by (simpl; field). apply Qle_shift_div_r. constructor. rewrite -> Qmult_comm. setoid_replace ((1#4)*d) with (proj1_sig ((1#4)*exist _ _ dpos)%Qpos) by reflexivity. rewrite des. unfold Qle; simpl. rewrite Zpos_mult_morphism. apply Z.le_trans with (Z.pos dn * Z.pos dd)%Z. rewrite Z.mul_comm, <- Z.le_mul_diag_r. apply Pos.le_1_l. reflexivity. apply Zmult_le_compat_l. 2: auto with *. rewrite Pos.of_nat_succ. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. rewrite <- (Nat.lt_succ_pred O _). apply le_n_S. exact Hm0. apply Pos2Nat.is_pos. discriminate. eapply FinSubset_ball_triangle_r;[|apply regFun_prf]. eapply FinSubset_ball_triangle_l;[apply regFun_prf|]. apply Hm1. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround CoRN.metric2.Prelength