proposition: Theorem Qnum_minus_distr_r : ∀ a b c, a - b # c == ((a # c) - (b # c)).
proof: Proof. intros a b c. unfold Qeq; simpl. rewrite Zmult_minus_distr_r. rewrite Zmult_plus_distr_l. rewrite Pos2Z.inj_mul. do 2 rewrite Zmult_assoc. do 2 rewrite Z.mul_opp_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz