proposition: Lemma set_finite_coinfinite_nat (s: nat -> Prop) : set_finite s -> set_coinfinite s.
proof: Proof. assert (LT: forall l x, In x l -> x <= fold_right Init.Nat.add 0 l). induction l; ins; desf; try apply IHl in H; lia. repeat autounfold with unfolderDb; red; ins; desf. tertium_non_datur (s (S (fold_right plus 0 findom + fold_right plus 0 findom0))) as [X|X]; [apply H in X | apply H0 in X]; apply LT in X; lia. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms