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