Library Coq.Reals.SplitRmult
Require Import Rbase.
Ltac split_Rmult :=
match goal with
| |- ((?X1 * ?X2)%R <> 0%R) =>
apply Rmult_integral_contrapositive; split; try split_Rmult
end.
Require Import Rbase.
Ltac split_Rmult :=
match goal with
| |- ((?X1 * ?X2)%R <> 0%R) =>
apply Rmult_integral_contrapositive; split; try split_Rmult
end.