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