proposition: Theorem Rtimes_neq_0 : forall n m : R, n ~= 0 /\ m ~= 0 -> n * m ~= 0.
proof: Proof. intros n m [H1 H2]. destruct (Rlt_trichotomy n 0) as [H3 | [H3 | H3]]; destruct (Rlt_trichotomy m 0) as [H4 | [H4 | H4]]; try (false_hyp H3 H1); try (false_hyp H4 H2). - apply Rneq_symm. apply Rlt_neq. now apply Rtimes_neg_neg. - apply Rlt_neq. rewrite Rtimes_comm. now apply Rtimes_pos_neg. - apply Rlt_neq. now apply Rtimes_pos_neg. - apply Rneq_symm. apply Rlt_neq. now apply Rtimes_pos_pos. Qed.
imports: Setoid Ring