proposition: Theorem Qpositive_plus_diff : forall w w' : Qpositive, w <> Qpositive_plus w w'.
proof: Proof. intros w w'; unfold Qpositive_plus in |- *; elim (interp_non_zero w); intros p (q, Heq); elim (interp_non_zero w'); intros p' (q', Heq'); rewrite Heq; rewrite Heq'. rewrite <- (construct_correct w _ _ (S p + S q) Heq). red in |- *; intros Heq2; cut (S p * (S q * S q') = (S p * S q' + S p' * S q) * S q). rewrite Nat.mul_add_distr_r. rewrite <- Nat.mul_assoc. rewrite (Nat.mul_comm (S q')). pattern (S p * (S q * S q')) at 1 in |- *. rewrite plus_n_O. intros H; apply Nat.add_cancel_l in H; simpl in |- *; discriminate H. apply Qpositive_c_equiv' with (S p + S q) (S p * S q' + S p' * S q + S q * S q'). auto with arith. auto with arith. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. auto. auto. auto. Qed.