proposition: Lemma eqpP : Equality.axiom eqp.
proof: Proof. move=> p q; apply: (iffP idP)=>[|<-]; last by rewrite /eqp Pos.compare_refl. rewrite /eqp; case e: ((p ?= q))%positive=> // _; exact: Pcompare_Eq_eq. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith