Definition natneq0andmult (n m : nat) : n ≠ 0 -> m ≠ 0 -> n * m ≠ 0. Proof. intros isn ism. induction n as [|n]. - apply fromempty. apply isn. - clear isn. simpl. apply natplusnonzero. assumption. Defined.