proposition: Theorem Qnat_succ : ∀ n x, x * Qnat (S n) == x * Qnat n + x.
proof: Proof. intros n x. unfold Qnat. setoid_replace x with (x * 1) at 3. rewrite <- Qmult_plus_distr_r. destruct (Qeq_dec x 0) as [Hz| ]; [ rewrite Hz; reflexivity | idtac ]. apply Qmult_inj_l; auto. unfold Qeq; simpl. do 2 rewrite Z.mul_1_r. rewrite Pos.mul_1_r, Z.add_1_r. apply Zpos_P_of_succ_nat. rewrite Qmult_comm, Qmult_1_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Psatz