diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 3 |
1 files changed, 3 insertions, 0 deletions
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 |