proposition: Lemma bottom x : unify_nz !=0 nz -> unify_r =0 cond -> False.
proof: Proof. by move: x => [x /= /andP[]]; move: cond nz => [[[]|]|] [] //= /[swap] ->. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)