proposition: Lemma widen_signed_subproof x nz' cond' : unify_nz nz' nz -> unify_r cond' cond -> Signed.spec x0 nz' cond' x%:num.
proof: Proof. case: x => [x /= /andP[]]. by case: cond nz cond' nz' => [[[]|]|] [] [[[]|]|] [] //= nz'' cond''; rewrite ?nz'' ?cond'' ?orbT //; move: cond'' nz'' => /eqP ->; rewrite lexx. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)