> module card where;

> import nat_ord;
> import set;

> [at_least_set [tau : U] = E_Nat ([_ : Nat] Set (Set (T tau))) (full (Set (T tau)))
>     [n : Nat] [Kn : Set (Set (T tau))] set (Set (T tau)) [A : Set (T tau)] ex tau [a : T tau]
>           and (in (T tau) a A) (in ? (setminus' tau A a) Kn)];
> [at_least [tau : U] [A : Set (T tau)] [n : Nat] = in ? A (at_least_set tau n)];
> [At_Least [tau : U] [A : Set (T tau)] [n : Nat] = In ? A (at_least_set tau n)];

> Claim At_Least_wd : (tau : U) (n : Nat) (A, B : Set (T tau)) Seteq (T tau) A B -> At_Least tau A n -> At_Least tau B n;
> Intros tau n' A' B' A'_is_B';
> Refine ImpE;
> Refine ImpE;
> Refine A'_is_B';
> Refine AllE ? [B : Set (T tau)] Imp (Seteq (T tau) A' B) (Imp (At_Least tau A' n') (At_Least tau B n'));
> Refine AllE ? [A : Set (T tau)] All ? [B : Set (T tau)] Imp (Seteq (T tau) A B) (Imp (At_Least tau A n') (At_Least tau B n'));
> Refine Big_Ind_Nat [n : Nat] All ? [A : Set (T tau)] All ? [B : Set (T tau)] Imp (Seteq (T tau) A B) (Imp (At_Least tau A n) (At_Least tau B n));
> 2 Refine AllI;
> 2 Intros A;
> Refine AllI;
> Intros B;
> Refine ImpI;
> Intros A_is_B;
> Refine ImpI;
> Intros A_atleast_0;
> Refine TrueI;
> ReturnAll;
> Intros n ih;
> Refine AllI;
> Intros A;
> Refine AllI;
> Intros B;
> Refine ImpI;
> Intros A_is_B;
> Refine ImpI;
> Refine ExE ? [a : T tau] And (In ? a A) (At_Least ? (setminus' ? A a) n);
> Intros a;
> Refine AndE;
> Intros a_in_A A0_atleast_n;
> Refine ExI ? [a : T tau] And (In ? a B) (At_Least ? (setminus' ? B a) n);
> 2 Refine a;
> Refine AndI;
> 2 Refine SeteqE ? A B a;
> 3 Refine A_is_B;
> 2 Refine a_in_A;
> Refine ImpE ? ? (ImpE ? ? (AllE ? ? ? (AllE ? ? ? ih)) ?) A0_atleast_n;
> Refine setminus'_wd;
> Refine A_is_B;
> ReturnAll;
> At_Least_wd;

> Claim at_least_1I : (tau : U) (A : Set (T tau)) (a : T tau) In (T tau) a A -> At_Least tau A (succ zero);
> Intros tau A a a_in_A;
> Refine ExI ? [x : T tau] And (In (T tau) x A) True;
> 2 Refine a;
> Refine AndI;
> Refine TrueI;
> Refine a_in_A;
> ReturnAll;
> at_least_1I;

> Claim at_least_1E : (tau : U) (A : Set (T tau)) At_Least tau A (succ zero) -> Ex (T tau) [a : T tau] In (T tau) a A;
> Intros tau A;
> Refine ExE ? [x : T tau] And (In (T tau) x A) True;
> Intros a;
> Refine AndE;
> Intros a_in_A _;
> Refine ExI;
> Refine a_in_A;
> ReturnAll;
> at_least_1E;

> Claim at_least_succ : (tau : U) (A : Set (T tau)) (n : Nat) At_Least tau A (succ n) -> At_Least tau A n;
> Intros tau A' n';
> Refine ImpE;
> Refine AllE ? [A : Set (T tau)] Imp (At_Least tau A (succ n')) (At_Least tau A n');
> Refine Big_Ind_Nat [n : Nat] All ? [A : Set (T tau)] Imp (At_Least tau A (succ n)) (At_Least tau A n);
> 2 Refine AllI;
> 2 Intros _;
> Refine ImpI;
> Intros _;
> Refine TrueI;
> ReturnAll;
> Intros n ih;
> Refine AllI;
> Intros A;
> Refine ImpI;
> Refine ExE ? [x : T tau] And (In ? x A) (At_Least tau (setminus' ? A x) (succ n));
> Intros a;
> Refine AndE;
> Intros a_in_A A0_atleast_Sn;
> Refine ExI ? [x : T tau] And (In ? x A) (At_Least tau (setminus' ? A x) n);
> 2 Refine a;
> Refine AndI;
> 2 Refine a_in_A;
> Refine ImpE ? ? ? A0_atleast_Sn;
> Refine AllE ? ? ? ih;
> ReturnAll;
> at_least_succ;

> Claim at_least_le : (tau : U) (A : Set (T tau)) (m, n : Nat) Le m n -> At_Least tau A n -> At_Least tau A m;
> Intros tau A m n m_le_n A_atleast_n;
> Refine LeE m n;
> Refine m_le_n;
> Intros p p_plus_m_is_n;
> Refine ImpE;
> 3 Refine (At_Least tau A (plus m p));
> Refine EqE' nat (At_Least tau A) (plus m p) n;
> Refine A_atleast_n;
> Refine trans nat ? (plus p m);
> Refine p_plus_m_is_n;
> Refine plus_comm;
> Refine Ind_Nat [p : Nat] imp (at_least tau A (plus m p)) (at_least tau A m);
> 2 Refine ImpI;
> 2 Intros A_atleast_m;
> Refine A_atleast_m;
> ReturnAll;
> Intros p' ih;
> Refine ImpI;
> Intros A_atleast_mSp';
> Refine ImpE;
> 2 Refine ih;
> Refine at_least_succ;
> Refine A_atleast_mSp';
> ReturnAll;
> at_least_le;

> Claim at_least_sub : (tau : U) (A, B : Set (T tau)) (n : Nat) Sub (T tau) A B -> At_Least tau A n -> At_Least tau B n;
> Intros tau A' B' n' A'_sub_B';
> Refine ImpE;
> Refine ImpE;
> Refine A'_sub_B';
> Refine AllE ? [B : Set (T tau)] Imp (Sub ? A' B) (Imp (At_Least ? A' n') (At_Least ? B n'));
> Refine AllE ? [A : Set (T tau)] All ? [B : Set (T tau)] Imp (Sub ? A B) (Imp (At_Least ? A n') (At_Least ? B n'));
> Refine Big_Ind_Nat [n : Nat] All ? [A : Set (T tau)] All ? [B : Set (T tau)] Imp (Sub ? A B) (Imp (At_Least ? A n) (At_Least ? B n));
> 2 Refine AllI;
> 2 Intros _;
> Refine AllI;
> Intros _;
> Refine ImpI;
> Intros _;
> Refine ImpI;
> Intros _;
> Refine TrueI;
> ReturnAll;
> Intros n ih;
> Refine AllI;
> Intros A;
> Refine AllI;
> Intros B;
> Refine ImpI;
> Intros A_sub_B;
> Refine ImpI;
> Refine ExE ? [x : T tau] And (In ? x A) (At_Least ? (setminus' ? A x) n);
> Intros x;
> Refine AndE;
> Intros x_in_A A0_atleast_n;
> Refine ExI ? [x : T tau] And (In ? x B) (At_Least ? (setminus' ? B x) n);
> 2 Refine x;
> Refine AndI;
> 2 Refine SubE ? A B x;
> 3 Refine A_sub_B;
> 2 Refine x_in_A;
> Refine ImpE;
> Refine A0_atleast_n;
> Refine ImpE;
> Refine setminus'_mono tau A B x;
> Refine A_sub_B;
> Refine AllE ? ? ? (AllE ? ? ? ih);
> ReturnAll;
> at_least_sub;

> Claim at_least_plus : (tau : U) (A : Set (T tau)) (a : T tau) (n : Nat) At_Least tau A n -> Not (In ? a A) ->
>   At_Least tau (setplus' tau A a) (succ n);
> Intros tau A' a n' AtleastA'n';
> Refine ImpE;
> Refine ImpE;
> Refine AtleastA'n';
> Refine AllE ? [A : ?] Imp (At_Least tau A n') (Imp (Not (In ? a A)) (At_Least ? (setplus' tau A a) (succ n')));
> Refine Big_Ind_Nat [n : Nat] All ? [A : ?] Imp (At_Least tau A n) (Imp (Not (In ? a A)) (At_Least ? (setplus' tau A a) (succ n)));
> 2 Refine AllI;
> 2 Intros A;
> Refine ImpI;
> Intros _;
> Refine ImpI;
> Intros _;
> Refine at_least_1I ? (setplus' tau A a) a;
> Refine OrI2;
> Refine EqI;
> ReturnAll;
> Intros n ih;
> Refine AllI;
> Intros A;
> Refine ImpI;
> Refine ExE ? [x : T tau] And (In (T tau) x A) (At_Least tau (setminus' tau A x) n);
> Intros x;
> Refine AndE;
> Intros x_in_A Ax_atleast_n;
> Refine ImpI;
> Intros a_notin_A;
> Refine ExI ? [x : T tau] And (In ? x (setplus' tau A a)) (At_Least tau (setminus' tau (setplus' tau A a) x) (succ n));
> 2 Refine x;
> Refine AndI;
> 2 Refine OrI1;
> 2 Refine x_in_A;
> Refine At_Least_wd; 
> 3 Refine (setplus' tau (setminus' tau A x) a);
> Refine ImpE ? ? (ImpE ? ? (AllE ? ? (setminus' tau A x) ih));
> Refine NotI;
> Refine AndE;
> Intros a_in_A _;
> Refine NotE;
> Refine a_in_A;
> Refine a_notin_A;
> ReturnAll;
> Refine Ax_atleast_n;
> Refine SeteqI;
> Intros y;
> Refine AndE;
> Intros y_in_Aa x_not_y;
> Refine OrE;
> Refine y_in_Aa;
> Refine OrI2;
> Intros y_in_A;
> Refine OrI1;
> Refine AndI;
> Refine x_not_y;
> Refine y_in_A;
> ReturnAll;
> Intros y;
> Refine OrE;
> Intros a_is_y;
> Refine AndI;
> Refine NotI;
> Intros x_is_y;
> Refine NotE;
> 2 Refine a_notin_A;
> Refine EqE ? ([z : T tau] In ? z A) x a;
> Refine transr ? ? ? y;
> Refine a_is_y;
> Refine x_is_y;
> Refine x_in_A;
> ReturnAll;
> Refine OrI2;
> Refine a_is_y;
> ReturnAll;
> Refine AndE;
> Intros y_in_A;
> Intros x_not_y;
> Refine AndI;
> Refine x_not_y;
> Refine OrI1;
> Refine y_in_A;
> ReturnAll;
> at_least_plus;

> Claim Subs_Elts : (tau : U) (X : Set (T tau)) (a, b : T tau) (n : Nat)
>  At_Least tau X n -> In ? a X -> Not (In ? b X) ->
>  At_Least ? (setplus' ? (setminus' ? X a) b) n;
> Intros tau X' a b n' X'_atleast_n' a_in_X';
> Refine ImpE;
> Refine ImpE;
> Refine a_in_X';
> Refine ImpE;
> Refine X'_atleast_n';
> Refine AllE ? [X : ?] Imp (At_Least tau X n') (Imp (In ? a X) (Imp (Not (In ? b X)) (At_Least tau (setplus' tau (setminus' ? X a) b) n')));
> Refine Big_Ind_Nat [n : Nat] All ? [X : ?] Imp (At_Least tau X n) (Imp (In ? a X) (Imp (Not (In ? b X)) (At_Least ? (setplus' ? (setminus' ? X a) b) n)));
> 2 Refine AllI;
> 2 Intros X;
> Refine ImpI;
> Intros _;
> Refine ImpI;
> Intros _;
> Refine ImpI;
> Intros _;
> Refine TrueI;
> ReturnAll;
> Intros n ih;
> Refine AllI;
> Intros X;
> Refine ImpI;
> Refine ExE ? [x : ?] And (In ? x X) (At_Least ? (setminus' ? X x) n);
> Intros x;
> Refine AndE;
> Intros x_in_X Xx_atleast_n;
> Refine ImpI;
> Intros a_in_X;
> Refine ImpI;
> Intros b_notin_X;
> Refine exmid (Eq tau a x);
> Intros a_not_x;
> Refine ExI ? [z : ?] And (In ? z (setplus' ? (setminus' ? X a) b)) (At_Least ? (setminus' ? (setplus' ? (setminus' ? X a) b) z) n);
> 2 Refine x;
> Refine AndI;
> 2 Refine OrI1;
> 2 Refine AndI;
> 3 Refine x_in_X;
> 2 Refine a_not_x;
> Refine At_Least_wd;
> 3 Refine (setplus' tau (setminus' tau (setminus' tau X x) a) b);
> Refine ImpE ? ? (ImpE ? ? (ImpE ? ? (AllE ? ? (setminus' tau X x) ih)));
> Refine NotI;
> Refine AndE;
> Intros b_in_X _;
> Refine NotE;
> Refine b_in_X;
> Refine b_notin_X;
> ReturnAll;
> Refine AndI;
> Refine NotI;
> Intros x_is_a;
> Refine NotE;
> 2 Refine a_not_x;
> Refine sym;
> Refine x_is_a;
> ReturnAll;
> Refine a_in_X;
> Refine Xx_atleast_n;
> Refine SeteqI;
> Intros z;
> Refine AndE;
> Intros z_in_Xab x_not_z;
> Refine OrE;
> Refine z_in_Xab;
> Refine OrI2;
> Refine AndE;
> Intros z_in_X a_not_z;
> Refine OrI1;
> Refine AndI;
> Refine a_not_z;
> Refine AndI;
> Refine x_not_z;
> Refine z_in_X;
> ReturnAll;
> Intros z;
> Refine OrE;
> Intros b_is_z;
> Refine AndI;
> Refine NotI;
> Intros x_is_z;
> Refine NotE;
> 2 Refine b_notin_X;
> Refine EqE ? ([z : ?] In ? z X) x b;
> Refine transr ? ? ? z;
> Refine b_is_z;
> Refine x_is_z;
> Refine x_in_X;
> ReturnAll;
> Refine OrI2;
> Refine b_is_z;
> ReturnAll;
> Refine AndE;
> Intros z_in_Xx a_not_z;
> Refine AndI;
> Refine AndE2 ? ? z_in_Xx;
> Refine OrI1;
> Refine AndI;
> Refine a_not_z;
> Refine AndE1 ? ? z_in_Xx;
> ReturnAll;
> Intros a_is_x;
> Refine ExI ? [z : ?] And (In ? z (setplus' ? (setminus' ? X a) b)) (At_Least ? (setminus' ? (setplus' ? (setminus' ? X a) b) z) n);
> 2 Refine b;
> Refine AndI;
> Refine At_Least_wd;
> Refine Xx_atleast_n;
> Refine SeteqI;
> Intros z;
> Refine AndE;
> Intros z_in_Xab b_not_z;
> Refine OrE;
> Refine z_in_Xab;
> Intros b_is_z;
> Refine NotE';
> Refine b_is_z;
> Refine b_not_z;
> ReturnAll;
> Refine AndE;
> Intros z_in_X a_not_z;
> Refine AndI;
> Refine NotI;
> Intros x_is_z;
> Refine NotE;
> 2 Refine a_not_z;
> Refine trans ? ? x;
> Refine x_is_z;
> Refine a_is_x;
> ReturnAll;
> Refine z_in_X;
> ReturnAll;
> Intros z;
> Refine AndE;
> Intros z_in_X x_not_z;
> Refine AndI;
> Refine NotI;
> Intros b_is_z;
> Refine NotE;
> 2 Refine b_notin_X;
> Refine EqE' ? ([z : ?] In ? z X) b z;
> Refine z_in_X;
> Refine b_is_z;
> ReturnAll;
> Refine OrI1;
> Refine AndI;
> Refine NotI;
> Intros a_is_z;
> Refine NotE;
> 2 Refine x_not_z;
> Refine transl ? a;
> Refine a_is_z;
> Refine a_is_x;
> ReturnAll;
> Refine z_in_X;
> ReturnAll;
> Refine OrI2;
> Refine EqI;
> ReturnAll;
> Subs_Elts;

> Claim TheoremR : (tau : U) (X : Set (T tau)) (x : T tau) (n : Nat)
>   At_Least tau X (succ n) ->
>   In ? x X ->
>   At_Least tau (setminus' tau X x) n;
> Intros tau X x n X_atleast_Sn x_in_X;
> Refine ExE ? [z : ?] And (In ? z X) (At_Least ? (setminus' ? X z) n);
> Refine X_atleast_Sn;
> Intros a;
> Refine AndE;
> Intros a_in_X Xa_atleast_n;
> Refine exmid (Eq tau a x);
> Intros a_not_x;
> Refine At_Least_wd;
> 3 Refine (setplus' tau (setminus' tau (setminus' tau X a) x) a);
> Refine Subs_Elts;
> Refine NotI;
> Refine AndE;
> Intros _ a_not_a;
> Refine NotE;
> 2 Refine a_not_a;
> Refine EqI;
> ReturnAll;
> Refine AndI;
> Refine a_not_x;
> Refine x_in_X;
> Refine Xa_atleast_n;
> Refine SeteqI;
> Intros z;
> Refine AndE;
> Intros z_in_X x_not_z;
> Refine exmid (Eq ? a z);
> Intros a_not_z;
> Refine OrI1;
> Refine AndI;
> Refine x_not_z;
> Refine AndI;
> Refine a_not_z;
> Refine z_in_X;
> ReturnAll;
> Refine OrI2;
> ReturnAll;
> Intros z;
> Refine OrE;
> Refine EqE tau ([z : T tau] In ? z (setminus' tau X x)) a z;
> Refine AndI;
> Refine NotI;
> Intros x_is_a;
> Refine NotE;
> 2 Refine a_not_x;
> Refine sym;
> Refine x_is_a;
> ReturnAll;
> Refine a_in_X;
> Refine AndE;
> Intros z_in_Xa x_not_z;
> Refine AndI;
> Refine x_not_z;
> Refine AndE1 ? ? z_in_Xa;
> ReturnAll;
> Refine EqE tau [z : T tau] At_Least tau (setminus' tau X z) n;
> Refine Xa_atleast_n;
> ReturnAll;
> TheoremR;

Cardinal Numbers

> [card [n : Nat] = set Nat [x : Nat] lt x n];
> [infty = full Nat];
> [card_num [A : Set Nat] = or (seteq nat A infty) (ex nat [n : Nat] seteq nat A (card n))];
> [Card_Num [A : Set Nat] = Or (Seteq Nat A infty) (Ex Nat [n : Nat] Seteq Nat A (card n))];

> [iscut [A : Set Nat] = all nat [m : Nat] all nat [n : Nat] imp (in Nat n A) (imp (le m n) (in Nat m A))];
> [IsCut [A : Set Nat] = All Nat [m : Nat] All Nat [n : Nat] Imp (In Nat n A) (Imp (Le m n) (In Nat m A))];

> Claim IsCutI : (A : Set Nat) ((m, n : Nat) In Nat n A -> Le m n -> In Nat m A) -> IsCut A;
> Intros A H;
> Refine AllI;
> Intros m;
> Refine AllI;
> Intros n;
> Refine ImpI;
> Intros n_in_A;
> Refine ImpI;
> Refine H;
> Refine n_in_A;
> ReturnAll;
> IsCutI;

> Claim IsCutE : (A : Set Nat) (m, n : Nat) IsCut A -> In Nat n A -> Le m n -> In Nat m A;
> Intros A m n Acut n_in_A;
> Refine ImpE;
> Refine ImpE;
> Refine n_in_A;
> Refine AllE Nat [y : Nat] Imp (In Nat y A) (Imp (Le m y) (In Nat m A));
> Refine AllE ? ? m Acut;
> ReturnAll;
> IsCutE;

> Claim IsCutwd : (A, B : Set Nat) Seteq Nat A B -> IsCut A -> IsCut B;
> Intros A B A_is_B Acut;
> Refine IsCutI;
> Intros m n n_in_B m_le_n;
> Refine SeteqE Nat A;
> Refine IsCutE;
> Refine m_le_n;
> Refine SeteqE' Nat A B;
> Refine n_in_B;
> Refine A_is_B;
> Refine Acut;
> Refine A_is_B;
> ReturnAll;
> IsCutwd;

> Claim full_cut : IsCut (full Nat);
> Refine IsCutI;
> Intros m n _ _;
> Refine TrueI;
> ReturnAll;
> full_cut;

> Claim card_cut : (n : Nat) IsCut (card n);
> Intros n;
> Refine IsCutI;
> Intros x y y_lt_n x_le_y;
> Refine Le_Lt_trans;
> Refine y_lt_n;
> Refine x_le_y;
> ReturnAll;
> card_cut;

> Claim pre_cut_card : (A : Set Nat) IsCut A -> Not (Seteq Nat A (full Nat)) ->
>    Ex Nat [n : Nat] Seteq Nat A (card n);
> Intros A Acut Anotfull;
> Refine ExE ? [n : Nat] Not (In ? n A);
> Refine Notall_Exnot ? [n : Nat] In Nat n A;
> Refine NotI;
> Intros allinA;
> Refine NotE;
> 2 Refine Anotfull;
> Refine SeteqI;
> Intros x _;
> Refine AllE ? ? ? allinA;
> ReturnAll;
> Intros x _;
> Refine TrueI;
> ReturnAll;
> Intros x';
> Refine ImpE;
> Refine Ind_Nat [x : Nat] imp (not (in Nat x A)) (ex nat [n : Nat] seteq nat A (card n));
> 2 Refine ImpI;
> 2 Intros zero_notin_A;
> Refine ExI Nat ([n : Nat] Seteq Nat A (card n)) zero;
> Refine SeteqI;
> Intros x x_lt_zero;
> Refine FalseE;
> Refine not_Lt_zero x x_lt_zero;
> ReturnAll;
> Intros x x_in_A;
> Refine NotE';
> 2 Refine zero_notin_A;
> Refine IsCutE;
> 2 Refine x_in_A;
> Refine zero_Le;
> Refine Acut;
> ReturnAll;
> Intros n ih;
> Refine ImpI;
> Intros sn_notin_A;
> Refine exmid (In Nat n A);
> Refine ImpE;
> Refine ih;
> Intros n_in_A;
> Refine ExI Nat ([n : Nat] Seteq Nat A (card n)) (succ n);
> Refine SeteqI;
> Intros x x_lt_sn;
> Refine IsCutE;
> 2 Refine n_in_A;
> 2 Refine Acut;
> Refine LtS_Le;
> Refine x_lt_sn;
> ReturnAll;
> Intros x x_in_A;
> Refine OrE;
> Refine Lt_or_Le x (succ n);
> 2 Intros x_lt_sn;
> Refine x_lt_sn;
> ReturnAll;
> Intros sn_le_x;
> Refine NotE';
> 2 Refine sn_notin_A;
> Refine IsCutE;
> Refine sn_le_x;
> Refine x_in_A;
> Refine Acut;
> ReturnAll;
> pre_cut_card;

> Claim cut_card_num : (A : Set Nat) IsCut A -> Card_Num A;
> Intros A Acut;
> Refine exmid (Seteq Nat A (full Nat));
> Intros A_not_full;
> Refine OrI2;
> Refine pre_cut_card;
> Refine A_not_full;
> Refine Acut;
> ReturnAll;
> Refine OrI1;
> ReturnAll;
> cut_card_num;

> Claim card_num_cut : (A : Set Nat) Card_Num A -> IsCut A;
> Intros A;
> Refine OrE;
> Refine ExE;
> Intros n A_is_card_n;
> Refine IsCutwd;
> 2 Refine Seteq_sym;
> 2 Refine A_is_card_n;
> Refine card_cut;
> ReturnAll;
> Intros A_is_infty;
> Refine IsCutwd;
> 2 Refine Seteq_sym;
> 2 Refine A_is_infty;
> Refine full_cut;
> ReturnAll;
> card_num_cut;

> Claim cut_total : (A, B : Set Nat) IsCut A -> IsCut B -> Or (Sub Nat A B) (Sub Nat B A);
> Intros A B Acut Bcut;
> Refine ImpI;
> Intros A_notsub_B;
> Refine SubI;
> Intros x x_in_B;
> Refine cont;
> Intros x_notin_A;
> Refine NotE;
> 2 Refine A_notsub_B;
> Refine SubI;
> Intros y y_in_A;
> Refine OrE;
> Refine Lt_or_Le x y;
> Intros y_le_x;
> Refine IsCutE;
> Refine y_le_x;
> Refine x_in_B;
> Refine Bcut;
> ReturnAll;
> Intros x_lt_y;
> Refine NotE';
> 2 Refine x_notin_A;
> Refine IsCutE;
> Refine Lt_Le;
> Refine x_lt_y;
> Refine y_in_A;
> Refine Acut;
> ReturnAll;
> cut_total;

> Claim le_card_sub : (m, n : Nat) Le m n -> Sub Nat (card m) (card n);
> Intros m n m_le_n;
> Refine SubI;
> Intros x x_lt_m;
> Refine Lt_Le_trans;
> Refine m_le_n;
> Refine x_lt_m;
> ReturnAll;
> le_card_sub;

> Claim at_least_cut : (tau : U) (A : Set (T tau)) IsCut (set Nat [x : Nat] at_least tau A (succ x));
> Intros tau A;
> Refine IsCutI;
> Intros m n A_atleast_sn m_le_n;
> Refine at_least_le tau A (succ m) (succ n);
> Refine A_atleast_sn;
> Refine succ_Le_succ;
> Refine m_le_n;
> ReturnAll;
> at_least_cut;

Cardinality

> [cardinality [tau : U] [A : Set (T tau)] = set Nat [n : Nat] at_least tau A (succ n)];

> Claim cardinality_wd : (tau : U) (A, B : Set (T tau)) Seteq (T tau) A B -> Seteq Nat (cardinality tau A) (cardinality tau B);
> Intros tau A B A_is_B;
> Refine SeteqI;
> Intros m;
> Refine At_Least_wd tau (succ m) B A;
> Refine Seteq_sym;
> Refine A_is_B;
> ReturnAll;
> Intros n;
> Refine At_Least_wd tau (succ n) A B;
> Refine A_is_B;
> ReturnAll;
> cardinality_wd;

> [exactly [tau : U] [A : Set (T tau)] [n : Nat] = seteq nat (cardinality tau A) (card n)];
> [Exactly [tau : U] [A : Set (T tau)] [n : Nat] = Seteq Nat (cardinality tau A) (card n)];

> Claim exactly_wd : (tau : U) (A, B : Set (T tau)) (n : Nat) Seteq (T tau) A B -> Exactly tau A n -> Exactly tau B n;
> Intros tau A B n A_is_B A_exactly_n;
> Refine Seteq_trans ? ? (cardinality tau A);
> Refine A_exactly_n;
> Refine cardinality_wd;
> Refine Seteq_sym;
> Refine A_is_B;
> ReturnAll;

> Claim exactly_le_atleast : (tau : U) (A : Set (T tau)) (m, n : Nat) Exactly tau A n -> Le m n -> At_Least tau A m;
> Intros tau A m n A_exactly_n m_le_n;
> Refine OrE;
> Refine zero_or_succ m;
> Refine ExE;
> Intros k m_is_Sk;
> Refine EqE' nat (At_Least tau A) m (succ k);
> Refine SeteqE' ? ? ? k A_exactly_n;
> Refine Lt_Le_trans ? (succ k);
> Refine EqE nat ([z : Nat] Le z n) m (succ k);
> Refine m_is_Sk;
> Refine m_le_n;
> Refine Lt_succ;
> Refine m_is_Sk;
> ReturnAll;
> Intros m_is_zero;
> Refine EqE' nat (At_Least tau A) m zero;
> Refine TrueI;
> Refine m_is_zero;
> ReturnAll;
> exactly_le_atleast;

> Claim exactly_atleast_le : (tau : U) (A : Set (T tau)) (m, n : Nat) Exactly tau A n -> At_Least tau A m -> Le m n;
> Intros tau A m n A_exactly_n A_atleast_m;
> Refine OrE;
> Refine zero_or_succ m;
> Refine ExE;
> Intros k m_is_Sk;
> Refine EqE' nat ([z : Nat] Le z n) m (succ k);
> Refine Lt_SLe;
> Refine SeteqE ? ? ? k A_exactly_n;
> Refine EqE nat (At_Least tau A) m (succ k);
> Refine m_is_Sk;
> Refine A_atleast_m;
> Refine m_is_Sk;
> ReturnAll;
> Intros m_is_zero;
> Refine EqE' nat ([z : Nat] Le z n) m zero;
> Refine zero_Le;
> Refine m_is_zero;
> ReturnAll;
> exactly_atleast_le;

> Claim leiffatleast_exactly : (tau : U) (A : Set (T tau)) (n : Nat)
>   ((m : Nat) Le m n -> At_Least tau A m) ->
>   ((m : Nat) At_Least tau A m -> Le m n) ->
>   Exactly tau A n;
> Intros tau A n H1 H2;
> Refine SeteqI;
> Intros x x_lt_n;
> Refine H1 (succ x);
> Refine Lt_SLe;
> Refine x_lt_n;
> ReturnAll;
> Intros x A_atleast_Sx;
> Refine SLe_Lt;
> Refine H2;
> Refine A_atleast_Sx;
> ReturnAll;
> leiffatleast_exactly;

> Claim exactly_atleast : (tau : U) (A : Set (T tau)) (n : Nat) Exactly tau A n -> At_Least tau A n;
> Intros tau A n A_exactly_n;
> Refine OrE;
> Refine zero_or_succ n;
> Refine ExE;
> Intros k n_is_Sk;
> Refine EqE' nat (At_Least tau A) n (succ k) n_is_Sk;
> Refine SeteqE' ? ? ? k A_exactly_n;
> Refine EqE' nat (Lt k) n (succ k) n_is_Sk;
> Refine Lt_succ;
> ReturnAll;
> Intros n_is_zero;
> Refine EqE' nat (At_Least tau A) n zero n_is_zero;
> Refine TrueI;
> ReturnAll;
> exactly_atleast;

> Claim exactly_notatleastS : (tau : U) (A : Set (T tau)) (n : Nat) Exactly tau A n -> Not (At_Least tau A (succ n));
> Intros tau A n A_exactly_n;
> Refine NotI;
> Intros A_atleast_Sn;
> Refine Lt_irref n;
> Refine SeteqE ? ? ? n A_exactly_n;
> Refine A_atleast_Sn;
> ReturnAll;
> exactly_notatleastS;

> Claim atleast_exactly : (tau : U) (A : Set (T tau)) (n : Nat) At_Least tau A n -> Not (At_Least tau A (succ n)) -> Exactly tau A n;
> Intros tau A n A_atleast_n not_A_atleast_Sn;
> Refine leiffatleast_exactly;
> Intros m A_atleast_m;
> Refine OrE;
> Refine Thm4_17 m n;
> Intros Sn_le_m;
> Refine NotE';
> 2 Refine not_A_atleast_Sn;
> Refine at_least_le;
> Refine A_atleast_m;
> Refine Sn_le_m;
> ReturnAll;
> Intros m_le_n;
> Refine m_le_n;
> ReturnAll;
> Intros m m_le_n;
> Refine at_least_le;
> Refine A_atleast_n;
> Refine m_le_n;
> ReturnAll;
> atleast_exactly;

> Claim exactly0E : (tau : U) (A : Set (T tau)) (x : T tau) Exactly tau A zero -> Not (In ? x A);
> Intros tau A x A_exactly_zero;
> Refine NotI;
> Intros x_in_A;
> Refine NotE;
> Refine at_least_1I tau A x;
> Refine x_in_A;
> Refine exactly_notatleastS tau A zero;
> Refine A_exactly_zero;
> ReturnAll;
> exactly0E;

> Claim exactly0I : (tau : U) (A : Set (T tau)) ((x : T tau) Not (In ? x A)) -> Exactly tau A zero;
> Intros tau A A_empty;
> Refine atleast_exactly;
> Refine NotI;
> Intros A_atleast_one;
> Refine ExE;
> 4 Refine T tau;
> Refine at_least_1E tau A;
> Refine A_atleast_one;
> Intros x;
> Refine NotE;
> Refine A_empty;
> ReturnAll;
> Refine TrueI;
> ReturnAll;
> exactly0I;

> Claim exactly_plus : (tau : U) (A : Set (T tau)) (a : T tau) (n : Nat)
>   Exactly tau A n -> Not (In ? a A) -> Exactly tau (setplus' tau A a) (succ n);
> Intros tau A a n A_exactly_n a_notin_A;
> Refine leiffatleast_exactly;
> Intros m Aa_atleast_m;
> Refine OrE;
> Refine zero_or_succ m;
> Refine ExE;
> Intros k m_is_Sk;
> Refine EqE' nat ([z : Nat] Le z (succ n)) m (succ k) m_is_Sk;
> Refine succ_Le_succ;
> Refine exactly_atleast_le tau A;
> Refine At_Least_wd;
> Refine TheoremR tau (setplus' tau A a) a;
> Refine OrI2;
> Refine EqI;
> Refine EqE nat (At_Least tau (setplus' tau A a)) m (succ k);
> Refine m_is_Sk;
> Refine Aa_atleast_m;
> Refine setminus'_setplus';
> Refine a_notin_A;
> Refine A_exactly_n;
> ReturnAll;
> Intros m_is_zero;
> Refine EqE' nat ([z : Nat] Le z (succ n)) m zero;
> Refine zero_Le;
> Refine m_is_zero;
> ReturnAll;
> Intros m m_le_Sn;
> Refine OrE;
> Refine zero_or_succ m;
> Refine ExE;
> Intros k m_is_Sk;
> Refine EqE' nat (At_Least tau (setplus' tau A a)) m (succ k);
> Refine at_least_plus;
> Refine a_notin_A;
> Refine exactly_le_atleast;
> 2 Refine A_exactly_n;
> Refine succ_Le_succ_cancel;
> Refine EqE nat ([z : Nat] Le z (succ n)) m (succ k);
> Refine m_is_Sk;
> Refine m_le_Sn;
> Refine m_is_Sk;
> ReturnAll;
> Intros m_is_zero;
> Refine EqE' nat (At_Least tau (setplus' tau A a)) m zero;
> Refine TrueI;
> Refine m_is_zero;
> ReturnAll;
> exactly_plus;

> Claim exactly_minus : (tau : U) (A : Set (T tau)) (a : T tau) (n : Nat)
>   Exactly tau A (succ n) -> In ? a A -> Exactly tau (setminus' tau A a) n;
> Intros tau A a n A_exactly_Sn a_in_A;
> Refine leiffatleast_exactly;
> Intros m Aa_atleast_m;
> Refine succ_Le_succ_cancel;
> Refine exactly_atleast_le;
> 4 Refine tau;
> 2 Refine A_exactly_Sn;
> Refine At_Least_wd;
> 2 Refine setplus'_setminus' tau A a;
> Refine at_least_plus tau (setminus' tau A a);
> Refine NotI;
> Refine AndE;
> Intros _;
> Intros a_not_a;
> Refine NotE;
> 2 Refine a_not_a;
> Refine EqI;
> ReturnAll;
> Refine Aa_atleast_m;
> Refine a_in_A;
> ReturnAll;
> Intros m m_le_n;
> Refine TheoremR;
> Refine a_in_A;
> Refine exactly_le_atleast;
> 2 Refine A_exactly_Sn;
> Refine succ_Le_succ;
> Refine m_le_n;
> ReturnAll;
> exactly_minus;

> Claim exactly_sub : (tau : U) (A : Set (T tau)) (a, b : T tau) (n : Nat)
>   Exactly tau A n -> In ? a A -> Not (In ? b A) -> Exactly tau (setplus' tau (setminus' tau A a) b) n;
> Intros tau A a b n A_exactly_n a_in_A b_notin_A;
> Refine OrE;
> Refine zero_or_succ n;
> Refine ExE;
> Intros k n_is_Sk;
> Refine EqE' nat (Exactly tau (setplus' tau (setminus' tau A a) b)) n (succ k);
> Refine exactly_plus tau (setminus' tau A a);
> Refine NotI;
> Refine AndE;
> Intros b_in_A _;
> Refine NotE;
> Refine b_in_A;
> Refine b_notin_A;
> ReturnAll;
> Refine exactly_minus;
> Refine a_in_A;
> Refine EqE nat (Exactly tau A) n;
> Refine n_is_Sk;
> Refine A_exactly_n;
> Refine n_is_Sk;
> ReturnAll;
> Intros n_is_zero;
> Refine NotE';
> Refine a_in_A;
> Refine exactly0E;
> Refine EqE nat (Exactly tau A);
> Refine n_is_zero;
> Refine A_exactly_n;
> ReturnAll;
> exactly_sub;

> Claim exactly_union : (tau : U) (A, B : Set (T tau)) (m, n : Nat)
>  Exactly tau A m -> Exactly tau B n -> Disjoint ? A B -> Exactly tau (union ? A B) (plus m n);
> Intros tau A B' m n' A_exactly_m B'_exactly_n';
> Refine ImpE;
> Refine ImpE;
> Refine B'_exactly_n';
> Refine AllE (Set (T tau)) [B : Set (T tau)] Imp (Exactly tau B n') (Imp (Disjoint (T tau) A B) (Exactly tau (union (T tau) A B) (plus m n')));
> Refine Big_Ind_Nat [n : Nat] All (Set (T tau)) [B : Set (T tau)] Imp (Exactly tau B n) (Imp (Disjoint (T tau) A B) (Exactly tau (union (T tau) A B) (plus m n)));
> Intros n ih;
> Refine AllI;
> Intros B;
> Refine ImpI;
> Intros B_exactly_Sn;
> Refine ImpI;
> Intros A_B_disjoint;
> Refine ExE (T tau) [b : T tau] And (In ? b B) (At_Least tau (setminus' tau B b) n);
> Refine exactly_atleast tau B (succ n) B_exactly_Sn;
> Intros b;
> Refine AndE;
> Intros b_in_B _;
> Refine exactly_wd tau (setplus' tau (union (T tau) A (setminus' tau B b)) b);
> Refine exactly_plus tau (union ? A (setminus' tau B b)) b (plus m n);
> Refine NotI;
> Refine OrE;
> Refine AndE;
> Intros _ b_not_b;
> Refine NotE;
> 2 Refine b_not_b;
> Refine EqI;
> ReturnAll;
> Intros b_in_A;
> Refine DisjointE (T tau) A B b;
> Refine b_in_B;
> Refine b_in_A;
> Refine A_B_disjoint;
> ReturnAll;
> Refine ImpE ? ? (ImpE ? ? (AllE ? ? (setminus' tau B b) ih));
> Refine DisjointI;
> Intros y y_in_A;
> Refine AndE;
> Intros y_in_B _;
> Refine DisjointE (T tau) A B y;
> Refine y_in_B;
> Refine y_in_A;
> Refine A_B_disjoint;
> ReturnAll;
> Refine exactly_minus;
> Refine b_in_B;
> Refine B_exactly_Sn;
> Refine SeteqI;
> Intros y;
> Refine OrE;
> Intros y_in_B;
> Refine exmid (Eq tau b y);
> Intros b_not_y;
> Refine OrI1;
> Refine OrI2;
> Refine AndI;
> Refine b_not_y;
> Refine y_in_B;
> ReturnAll;
> Refine OrI2;
> ReturnAll;
> Intros y_in_A;
> Refine OrI1;
> Refine OrI1;
> Refine y_in_A;
> ReturnAll;
> Intros y;
> Refine OrE;
> Intros b_is_y;
> Refine OrI2;
> Refine EqE tau ([z : T tau] In (T tau) z B) b y;
> Refine b_is_y;
> Refine b_in_B;
> ReturnAll;
> Refine OrE;
> Refine AndE;
> Intros y_in_B _;
> Refine OrI2;
> Refine y_in_B;
> ReturnAll;
> Refine OrI1;
> ReturnAll;
> Refine AllI;
> Intros B;
> Refine ImpI;
> Intros B_exactly_0;
> Refine ImpI;
> Intros A_B_disjoint;
> Refine exactly_wd;
> Refine A_exactly_m;
> Refine SeteqI;
> Intros x;
> Refine OrE;
> Refine NotE';
> Refine exactly0E tau B x;
> Refine B_exactly_0;
> Intros x_in_A;
> Refine x_in_A;
> ReturnAll;
> Intros x;
> Refine OrI1;
> ReturnAll;
> exactly_union;

> Claim exactly_card : (n : Nat) Exactly nat (card n) n;
> Refine Ind_Nat [n : Nat] exactly nat (card n) n;
> Intros n n_exactly_n;
> Refine exactly_wd nat (setplus' nat (card n) n) (card (succ n)) (succ n);
> Refine exactly_plus nat (card n) n;
> Refine NotI;
> Refine Lt_irref;
> Refine n_exactly_n;
> Refine SeteqI;
> Intros x x_lt_Sn;
> Refine OrE;
> Refine Le_Lt_or_eq x n;
> Refine LtS_Le;
> Refine x_lt_Sn;
> Intros x_is_n;
> Refine OrI2;
> Refine sym;
> Refine x_is_n;
> ReturnAll;
> Refine OrI1;
> ReturnAll;
> Intros x;
> Refine OrE;
> Refine EqE nat ([z : Nat] In Nat z (card (succ n))) n x;
> Refine Lt_succ;
> Intros x_lt_n;
> Refine Lt_trans x n (succ n);
> Refine Lt_succ;
> Refine x_lt_n;
> ReturnAll;
> Refine exactly0I nat (card zero);
> Intros x;
> Refine NotI;
> Refine not_Lt_zero;
> ReturnAll;
> exactly_card;