proposition: Lemma lt0F x : unify_r >=0 cond -> x%:num < x0 :> T = false.
proof: Proof. by move=> ?; rewrite le_gtF//; apply: ge0. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)