proposition: Theorem Qpositive_mult_One : forall w : Qpositive, Qpositive_mult One w = w.
proof: Proof. intros w; elim (interp_non_zero w); intros p Hex; elim Hex; intros q Heq. unfold Qpositive_mult in |- *. replace (Qpositive_i One) with (1, 1). rewrite Heq. repeat rewrite Nat.mul_1_l. apply construct_correct; auto with *. simpl in |- *; auto. Qed.