proposition: Lemma eq0 x : unify_r =0 cond -> x%:num = x0.
proof: Proof. by case: x => [x /= /andP[_]]; move: cond nz => [[[]|]|] [] //= /eqP ->. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)