fact: Definition eqp (p q : positive) : bool := match ((p ?= q))%positive with Eq => true | _ => false end.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith