proposition: Theorem Qmult_minus_distr_l : ∀ x y z, (x - y) * z == x * z - y * z.
proof: Proof. intros x y z. unfold Qminus. rewrite Qmult_plus_distr_l. rewrite Qmult_opp_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz