fact: Definition comparePc T (eq_dec : comparable T) : Equality.axiom eq_dec := fun x y => match eq_dec x y as s return reflect (x = y) s with | left a => ReflectT (x = y) a | right b => ReflectF (x = y) b end.
imports: mathcomp(all_ssreflect)