proposition: Theorem Qmult_compat_l : ∀ a b c, a == b → c * a == c * b.
proof: Proof. intros a b c H. destruct (Qeq_dec c 0) as [Hz| ]; [ rewrite Hz; reflexivity | idtac ]. apply Qmult_inj_l; assumption. Qed.
imports: Utf8 QArith Field2