proposition: Lemma sign_mult (x y : R) : sign (x * y) = sign x * sign y.
proof: Proof. wlog: x / (0 < x) => [Hw | Hx]. case: (Rle_lt_dec 0 x) => Hx. case: Hx => Hx. by apply Hw. rewrite -Hx Rmult_0_l. rewrite sign_0. by rewrite Rmult_0_l. rewrite -(Ropp_involutive x). rewrite sign_opp Ropp_mult_distr_l_reverse sign_opp Hw. ring. by apply Ropp_0_gt_lt_contravar. wlog: y / (0 < y) => [Hw | Hy]. case: (Rle_lt_dec 0 y) => Hy. case: Hy => Hy. by apply Hw. rewrite -Hy Rmult_0_r. rewrite sign_0. by rewrite Rmult_0_r. rewrite -(Ropp_involutive y). rewrite sign_opp Ropp_mult_distr_r_reverse sign_opp Hw. ring. by apply Ropp_0_gt_lt_contravar. have Hxy : 0 < x * y. by apply Rmult_lt_0_compat. rewrite -> 3!sign_eq_1 by easy. by rewrite Rmult_1_l. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)