proposition: Theorem R_uncountable : forall u : nat -> R, ~Bijective u.
proof: Proof. intros u [v [H3 H4]]. pose proof (conj H4 H3) as H. assert (forall n : nat, n + v (fst (proj1_sig (tearing_sequences u v H 1))) <= v (fst (proj1_sig (tearing_sequences u v H (S n))))). { induction n. - simpl. apply Nat.le_refl. - apply (Nat.le_trans (S n + v (fst (proj1_sig (tearing_sequences u v H 1)))) (S (v (fst (proj1_sig (tearing_sequences u v H (S n))))))). + simpl. apply -> Nat.succ_le_mono. assumption. + apply first_indices_increasing. intro H1. discriminate. } assert (v (proj1_sig (torn_number u v H)) + v (fst (proj1_sig (tearing_sequences u v H 1))) < v (proj1_sig (torn_number u v H))). { pose proof (limit_index_above_all_indices u v H (v (proj1_sig (torn_number u v H)))). specialize (H0 (v (proj1_sig (torn_number u v H)))). apply (Nat.le_lt_trans (v (proj1_sig (torn_number u v H)) + v (fst (proj1_sig (tearing_sequences u v H 1)))) (v (fst (proj1_sig (tearing_sequences u v H (S (v (proj1_sig (torn_number u v H))))))))). - assumption. - assumption. } assert (forall n m : nat, ~(n + m < n)). { induction n. - intros. intro H2. inversion H2. - intro m. intro H2. simpl in H2. apply Nat.lt_succ_lt_pred in H2. simpl in H2. apply IHn in H2. contradiction. } apply H2 in H1. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon