diff options
Diffstat (limited to 'mathcomp/ssrtest/wlog_suff.v')
| -rw-r--r-- | mathcomp/ssrtest/wlog_suff.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/wlog_suff.v b/mathcomp/ssrtest/wlog_suff.v new file mode 100644 index 0000000..4e1c86d --- /dev/null +++ b/mathcomp/ssrtest/wlog_suff.v @@ -0,0 +1,16 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +Require Import ssreflect ssrbool. + +Lemma test b : b || ~~b. +wlog _ : b / b = true. + case: b; [ by apply | by rewrite orbC ]. +wlog suff: b / b || ~~b. + by case: b. +by case: b. +Qed. + +Lemma test2 b c (H : c = b) : b || ~~b. +wlog _ : b {c H} / b = true. + by case: b H. +by case: b. +Qed.
\ No newline at end of file |