proposition: Theorem Qplus_div : ∀ x y z, ¬(z == 0) → x + y / z == (x * z + y) / z.
proof: Proof. intros x y z Hc. rewrite Qdiv_plus_distr_r. rewrite Qdiv_mult_l; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Sorted Psatz