Question: Problem with assume and additionally

Could you please look at the following piace of code:


The result of last command is


that is not z:=d~t=a.

If I skip the command additionally(d≠0): then everything is good. However I need this command. Could you help to handle this problem?

Please Wait...