index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
bugs
/
opened
/
shouldnotfail
/
1449.v
blob: d9695360f909f62a5ed4622ce44e2b789b2a3818 (
plain
)
1
2
3
4
5
Require
Import
Arith
.
Goal
0
<=
0.
eapply
le_trans
.
setoid_rewrite
mult_comm
.