Cardinals: Remove ge_cardinal and gt_cardinal

These notions are redundant. If they are used in lemmas, they make it harder to `Search` for results.
coq-community · Aug 6, 2024 · c020d2d · c020d2d
1 parent 519dc58
commit c020d2d
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/theories/ZornsLemma/Cardinals/Cardinals.v b/theories/ZornsLemma/Cardinals/Cardinals.v
@@ -16,10 +16,6 @@ Definition eq_cardinal (X Y : Type) : Prop :=
 
 Definition lt_cardinal (kappa lambda:Type) : Prop :=
   le_cardinal kappa lambda /\ ~ eq_cardinal kappa lambda.
-Definition ge_cardinal (kappa lambda:Type) : Prop :=
-  le_cardinal lambda kappa.
-Definition gt_cardinal (kappa lambda:Type) : Prop :=
-  lt_cardinal lambda kappa.
 
 Instance le_cardinal_preorder : PreOrder le_cardinal.
 Proof.