proposition: Lemma Qpos_plus_strext : bin_fun_strext Qpos_as_CSetoid Qpos_as_CSetoid Qpos_as_CSetoid Qpos_plus.
proof: Proof. red in |- *. simpl in |- *. intros x1 x2 y1 y2 H. destruct (Qeq_dec x1 x2)as [A|A];[|tauto]. right. autorewrite with QposElim in H. intros B. apply H. rewrite -> A. rewrite -> B. reflexivity. Qed.
imports: CoRN.model.setoids.Qsetoid CoRN.algebra.CSetoidFun CoRN.model.structures.Qpossec