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
.