proposition: Lemma associative_Qpos_plus : associative Qpos_plus.
proof: Proof. unfold associative in |- *. intros x y z. simpl. autorewrite with QposElim. apply Qplus_is_assoc. Qed.
imports: CoRN.model.setoids.Qsetoid CoRN.algebra.CSetoidFun CoRN.model.structures.Qpossec