Add valid_paren_cnt_eq

babaeee · Feb 1, 2024 · f74e0d5 · f74e0d5
1 parent e2bf40c
commit f74e0d5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/library/EnumerativeCombinatorics.v b/library/EnumerativeCombinatorics.v
@@ -1174,6 +1174,7 @@ Proof;
     lia;
 Qed;
 Todo valid_paren_cnt_right: ∀ a, valid_paren a -> ∀ k, 2 * k = |a| -> cnt ')' a = k;
+Todo valid_paren_cnt_eq: ∀ a, valid_paren a -> cnt '(' a = cnt ')' a;
 
 Theorem count_of_lists: ∀ T: U, ∀ S: set T, ∀ m, 0 < m -> |S| = m -> ∀ n, 0 ≤ n -> |{ l: list T | member_set l ⊆ S ∧ |l| = n }| = m ^ n;
 Proof;