proposition: Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0.
proof: Proof. intros n m; split; [intro H | intros [H1 H2]]. - apply lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. + now split. + false_hyp H1 nlt_0_r. - now apply mul_pos_pos. Qed.
imports: NAddOrder