Initial commit

1 files changed, 12 insertions, 0 deletions

diff --git a/mathcomp/ssrtest/occarrow.v b/mathcomp/ssrtest/occarrow.v
new file mode 100644
index 0000000..deaee0c
--- /dev/null
+++ b/mathcomp/ssrtest/occarrow.v
@@ -0,0 +1,12 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect eqtype ssrnat.
+
+Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n.
+move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-.
+by move: E => {3}->.
+Qed.
+
+Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m).
+by move=> n m; constructor=> [|{2}->].
+Qed.
+