proposition: Theorem interp_inject : forall w w' : Qpositive, Qpositive_i w = Qpositive_i w' -> w = w'.
proof: Proof. intros w w' H; CaseEq (Qpositive_i w). intros p q Heq. rewrite <- construct_correct with (1 := Heq) (n := p + q). apply construct_correct; auto. rewrite <- H; auto. auto. Qed.