path: root/coq/ex/mult2.v

Require Import mult1.

Definition bar:bool := if le_lt_dec foo 0 then true else false.