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