fact: Definition ap_Qpos_is_apartness := Build_is_CSetoid _ _ _ ap_Qpos_irreflexive1 ap_Qpos_symmetric1 ap_Qpos_cotransitive1 ap_Qpos_tight1.
imports: CoRN.model.setoids.Qsetoid CoRN.algebra.CSetoidFun CoRN.model.structures.Qpossec