aboutsummaryrefslogtreecommitdiff
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.