proposition: Lemma eqzP : Equality.axiom Zeq_bool.
proof: Proof. by move=> z1 z2; apply: (iffP idP); move/Zeq_is_eq_bool. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith