proposition: Lemma ap_Qpos_cotransitive1 : cotransitive (A:=Qpos) Qap.
proof: Proof. red in |- *. intros; apply ap_Q_cotransitive0; auto. Qed.
imports: CoRN.model.setoids.Qsetoid CoRN.algebra.CSetoidFun CoRN.model.structures.Qpossec