proposition: Lemma sign0 : sign 0 = 0 :> G.
proof: Proof. Proof . by rewrite /sign !ltr_irrefl . Qed . Lemma sign0P : forall x, reflect (sign x = 0) (x == 0) . Proof . move=> x; rewrite /sign; case: (compareP 0 x)=> H; last first. + by rewrite -H eqxx; constructor. + rewrite (negbTE (ltr_ne H)); constructor. by apply/eqP; rewrite oppr_eq0 nonzero1r. + rewrite eq_sym (negbTE (ltr_ne H)); constructor. by apply/eqP; rewrite nonzero1r. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)