proposition: Lemma eq0F x : unify_nz !=0 nz -> x%:num == x0 :> T = false.
proof: Proof. by move=> /neq0-/(_ x)/negPf->. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)