proposition: Lemma Rmult_integral1 r1 r2 : r1 * r2 = 0 -> r1 = 0 \/ r2 = 0.
proof: Proof. intros Hm. destruct (Req_dec r1 0) as [ZR1|ZNR1]; [left; assumption | right]. replace r2 with (r1 * r2 / r1); [idtac | field; assumption]. rewrite Hm; field; assumption. Qed.
imports: Reals Psatz