proposition: Lemma sign_negR : forall x, x <<! 0 -> sign x = -1 .
proof: Proof. Proof . by move=> x hx; rewrite /sign hx (negbTE (ltrN hx)). Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)