Merge pull request #1947 from Alizter/ps/rr/bool__add_convenient_vari…

…ant_of_negb_ne Bool: add convenient variant of negb_ne
HoTT · May 4, 2024 · 72ced09 · 72ced09
2 parents 010c169 + bfb2b40
commit 72ced09
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v
@@ -92,6 +92,16 @@ Proof.
   - intros oops; case (oops idpath).
 Defined.
 
+(** This version of [negb_ne] is more convenient to [destruct] against. *)
+Definition negb_ne' {b1 b2 : Bool}
+  : (b1 <> b2) -> (negb b1 = b2).
+Proof.
+  intros oops.
+  symmetry.
+  apply negb_ne.
+  exact (symmetric_neq oops).
+Defined.
+
 (** ** Products as [forall] over [Bool] *)
 
 Section BoolForall.