added proofs about addition chain exponentiation for later use in ModularBaseSystem [pow], which we need for sqrt and inversion.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/Option.v b/src/Util/Option.v
index db4b69dde..2c11771ff 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -60,3 +60,12 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect
          | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
            => change (option_rect P S N (Some x)) with (S x); cbv beta
          end.
+
+Definition option_eq {A} eq (x y : option A) :=
+  match x with
+  | None    => y = None
+  | Some ax => match y with
+               | None => False
+               | Some ay => eq ax ay
+               end
+  end.