From d2712446da700450239dd5556431b0d40a446dde Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Aug 2018 21:35:12 -0400 Subject: Add ZRange.union_comm --- src/Util/ZRange/BasicLemmas.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 1245bfe3f..d48c89011 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -43,6 +43,9 @@ Module ZRange. Definition normalize_or v : normalize v = v \/ normalize v = flip v. Proof. t. Qed. + Lemma union_comm r1 r2 : union r1 r2 = union r2 r1. + Proof. t. Qed. + Local Ltac t2_step := first [ t_step | rewrite !Bool.andb_true_iff -- cgit v1.2.3