proposition: Theorem Qdiv_minus_distr_r : ∀ x y z, (x - y) / z == x / z - y / z.
proof: Proof. intros x y z. destruct (Qeq_dec z 0) as [Heq| Hne]. rewrite Heq. unfold Qdiv, Qinv; simpl. do 3 rewrite Qmult_0_r. reflexivity. field; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz