Add lemma: ge0_fsize (#701)

EasyCrypt · Feb 4, 2025 · 649a1ba · 649a1ba
1 parent 782eb5c
commit 649a1ba
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/theories/datatypes/FMap.ec b/theories/datatypes/FMap.ec
@@ -734,6 +734,9 @@ op fsize (m : ('a,'b) fmap) : int = FSet.card (fdom m).
 lemma fsize_empty ['a 'b] : fsize<:'a,'b> empty = 0. 
 proof. by rewrite /fsize fdom0 fcards0. qed.
 
+lemma ge0_fsize (m : ('a, 'b) fmap) : 0 <= fsize m.
+proof. by rewrite fcard_ge0. qed. 
+
 lemma fsize_set (m : ('a, 'b) fmap) k v : 
   fsize m.[k <- v] = b2i (k \notin m) + fsize m.
 proof. by rewrite /fsize fdom_set fcardU1 mem_fdom. qed.