proposition: Lemma sgr_cp0 x : ((sg x == 1) = (0 < x)) * ((sg x == -1) = (x < 0)) * ((sg x == 0) = (x == 0)).
proof: Proof. rewrite -[1]/((-1) ^+ false) -signrN lt0r leNgt sgr_def. case: (x =P 0) => [-> | _]; first by rewrite !(eq_sym 0) !signr_eq0 ltxx eqxx. by rewrite !(inj_eq signr_inj) eqb_id eqbF_neg signr_eq0 //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)