proposition: Lemma rmul_reg_l p q1 q2 : ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
proof: Proof. intros H EQ. assert (H' : p * (q1 / p) == p * (q2 / p)). { now rewrite !rdiv_def, !rmul_assoc, EQ. } now rewrite !rdiv_simpl in H'. Qed.
imports: ZArith_base