forall a b:Z, 0 < b -> {q:Z &{r:Z | a=q*b + r /\ 0 <= r < b}}instead of
forall a b:Z, 0 <= b -> {q:Z &{r:Z | a=q*b + r /\ 0 <= r < b}}
Inductive sum (A B : Type) : Type := inl : A -> A + B | inr : B -> A + BThe function div2_gen uses sum and not sumbool, since (div2_of_even _ _) returns a term of sort Set (hence Type) and not a proposition.