proposition: Lemma ap_nat_cotransitive0 : forall x y : nat, (x{#N}y) -> forall z : nat, (x{#N}z) or (z{#N}y).
proof: Proof. intros x y X z. unfold ap_nat in |- *. case (eq_nat_dec x z). intro e. right. rewrite <- e. assumption. intro. left. intro. elim n. assumption. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)