proposition: Lemma countable_nat_product: CountableT (nat * nat).
proof: Proof. pose (sum_1_to_n := fix sum_1_to_n n:nat := match n with | O => O | S m => (sum_1_to_n m) + n end). exists (fun p:nat*nat => let (m,n):=p in (sum_1_to_n (m+n)) + n). assert (forall m n:nat, m<n -> sum_1_to_n m + m < sum_1_to_n n). - intros. induction H. + simpl. auto with arith. + apply Nat.lt_trans with (sum_1_to_n m0); trivial. assert (sum_1_to_n m0 + 0 < sum_1_to_n m0 + S m0) by auto with arith. assert (sum_1_to_n m0 + 0 = sum_1_to_n m0) by auto with arith. now rewrite H1 in H0. - intros [x1 y1] [x2 y2] H0. case (lt_eq_lt_dec (x1+y1) (x2+y2)); intro. + case s; intro. * assert (sum_1_to_n (x1+y1) + y1 < sum_1_to_n (x2+y2) + y2); try lia. apply Nat.le_lt_trans with (sum_1_to_n (x1+y1) + (x1+y1)); try lia. apply Nat.lt_le_trans with (sum_1_to_n (x2+y2)); try lia. apply H. lia. * assert (y1=y2) by (rewrite e in H0; lia). f_equal; lia. + cut (sum_1_to_n (x2+y2) + y2 < sum_1_to_n (x1+y1) + y1); try lia. apply Nat.le_lt_trans with (sum_1_to_n (x2+y2) + (x2+y2)), Nat.lt_le_trans with (sum_1_to_n (x1+y1)); auto with arith. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)