diff options
Diffstat (limited to 'theories/Reals/SplitRmult.v')
| -rw-r--r-- | theories/Reals/SplitRmult.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 71b2ebf215..281745a11e 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -11,9 +11,10 @@ (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) -Require Rbase. - -Recursive Tactic Definition SplitRmult := - Match Context With - | [ |- ~(Rmult ?1 ?2)==R0 ] -> Apply mult_non_zero; Split;Try SplitRmult. +Require Import Rbase. +Ltac split_Rmult := + match goal with + | |- ((?X1 * ?X2)%R <> 0%R) => + apply Rmult_integral_contrapositive; split; try split_Rmult + end. |