proposition: Lemma R_ap_cotrans : cotransitive R_ap.
proof: Proof. red in |- *; intros x y Hxy z. elim Hxy; intro H; elim (R_lt_cotrans _ _ H z); unfold R_ap in |- *; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection