Description: Lemma for mulgt0con1d . Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024)