proposition: Lemma widen_signedE x (unz : unify_nz nz nz) (ucond : unify_r cond cond) : @widen_signed x nz cond unz ucond = x.
proof: Proof. exact/val_inj. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)