Closed thery closed 3 years ago
in transc.ml lime 2605 : let TAN_ADD = prove( !x y. ~(cos(x) = &0) /\ ~(cos(y) = &0) /\ ~(cos(x + y) = &0) ==> (tan(x + y) = (tan(x) + tan(y)) / (&1 - tan(x) * tan(y))),
!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0) /\ ~(cos(x + y) = &0) ==> (tan(x + y) = (tan(x) + tan(y)) / (&1 - tan(x) * tan(y)))
the assumption ~(cos(x + y) = &0) seems unnecessary.
my bad, you don't have inv(0) = 0
inv(0) = 0
thery
commented
3 years ago thery
commented
3 years ago
in transc.ml lime 2605 : let TAN_ADD = prove(
!x y. ~(cos(x) = &0) /\ ~(cos(y) = &0) /\ ~(cos(x + y) = &0) ==> (tan(x + y) = (tan(x) + tan(y)) / (&1 - tan(x) * tan(y))),the assumption ~(cos(x + y) = &0) seems unnecessary.